Module Ptree_helpers.F

module F: sig .. end

Extra helpers for creating declarations in top-down style, functional interface

type state

val create : unit -> state

val begin_module : state -> ?loc:Loc.position -> string -> state

val use : state ->
       ?loc:Loc.position -> import:bool -> string list -> state

see use_import above

val add_prop : state ->
       Decl.prop_kind ->
       ?loc:Loc.position -> string -> Ptree.term -> state

val begin_let : state ->
       ?ghost:bool ->
       ?ret_type:Ptree.pty -> string -> Ptree.binder list -> state

val add_pre : state -> Ptree.term -> state

val add_post : state -> Ptree.term -> state

val add_body : state -> Ptree.expr -> state

val end_module : state -> state

val get_mlw_file : state -> Ptree.mlw_file