sig
type state
val create : unit -> Ptree_helpers.F.state
val begin_module :
Ptree_helpers.F.state ->
?loc:Loc.position -> string -> Ptree_helpers.F.state
val use :
Ptree_helpers.F.state ->
?loc:Loc.position -> import:bool -> string list -> Ptree_helpers.F.state
val add_prop :
Ptree_helpers.F.state ->
Decl.prop_kind ->
?loc:Loc.position -> string -> Ptree.term -> Ptree_helpers.F.state
val begin_let :
Ptree_helpers.F.state ->
?ghost:bool ->
?ret_type:Ptree.pty ->
string -> Ptree.binder list -> Ptree_helpers.F.state
val add_pre : Ptree_helpers.F.state -> Ptree.term -> Ptree_helpers.F.state
val add_post : Ptree_helpers.F.state -> Ptree.term -> Ptree_helpers.F.state
val add_body : Ptree_helpers.F.state -> Ptree.expr -> Ptree_helpers.F.state
val end_module : Ptree_helpers.F.state -> Ptree_helpers.F.state
val get_mlw_file : Ptree_helpers.F.state -> Ptree.mlw_file
end