Module Ptree_helpers.I

module I: sig .. end

Extra helpers for creating declarations in top-down style, imperative interface. Beware that these functions are not thread-safe

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

see begin_module above

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

see use_import above

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

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

val add_pre : Ptree.term -> unit

val add_post : Ptree.term -> unit

val add_body : Ptree.expr -> unit

val end_module : unit -> unit

val get_mlw_file : unit -> Ptree.mlw_file