sig
  val ident :
    ?attrs:Why3.Ptree.attr list ->
    ?loc:Why3.Loc.position -> string -> Why3.Ptree.ident
  val qualid : string list -> Why3.Ptree.qualid
  val const :
    ?kind:Why3.Number.int_literal_kind -> int -> Why3.Constant.constant
  val unit_binder : ?loc:Why3.Loc.position -> unit -> Why3.Ptree.binder list
  val one_binder :
    ?loc:Why3.Loc.position ->
    ?ghost:bool -> ?pty:Why3.Ptree.pty -> string -> Why3.Ptree.binder list
  val term :
    ?loc:Why3.Loc.position -> Why3.Ptree.term_desc -> Why3.Ptree.term
  val tconst : ?loc:Why3.Loc.position -> int -> Why3.Ptree.term
  val tvar : ?loc:Why3.Loc.position -> Why3.Ptree.qualid -> Why3.Ptree.term
  val tapp :
    ?loc:Why3.Loc.position ->
    Why3.Ptree.qualid -> Why3.Ptree.term list -> Why3.Ptree.term
  val pat :
    ?loc:Why3.Loc.position -> Why3.Ptree.pat_desc -> Why3.Ptree.pattern
  val pat_var :
    ?loc:Why3.Loc.position -> Why3.Ptree.ident -> Why3.Ptree.pattern
  val break_id : string
  val continue_id : string
  val return_id : string
  val expr :
    ?loc:Why3.Loc.position -> Why3.Ptree.expr_desc -> Why3.Ptree.expr
  val econst : ?loc:Why3.Loc.position -> int -> Why3.Ptree.expr
  val eapp :
    ?loc:Why3.Loc.position ->
    Why3.Ptree.qualid -> Why3.Ptree.expr list -> Why3.Ptree.expr
  val eapply :
    ?loc:Why3.Loc.position ->
    Why3.Ptree.expr -> Why3.Ptree.expr -> Why3.Ptree.expr
  val evar : ?loc:Why3.Loc.position -> Why3.Ptree.qualid -> Why3.Ptree.expr
  val empty_spec : Why3.Ptree.spec
  val use :
    ?loc:Why3.Loc.position -> import:bool -> string list -> Why3.Ptree.decl
  val global_var_decl :
    Why3.Ptree.pty -> string -> Why3.Ptree.ident * Why3.Ptree.decl
  module F :
    sig
      type state
      val create : unit -> Ptree_helpers.F.state
      val begin_module :
        Ptree_helpers.F.state ->
        ?loc:Why3.Loc.position ->
        ?intf:Why3.Ptree.qualid -> string -> Ptree_helpers.F.state
      val use :
        Ptree_helpers.F.state ->
        ?loc:Why3.Loc.position ->
        import:bool -> string list -> Ptree_helpers.F.state
      val add_prop :
        Ptree_helpers.F.state ->
        Why3.Decl.prop_kind ->
        ?loc:Why3.Loc.position ->
        string -> Why3.Ptree.term -> Ptree_helpers.F.state
      val add_global_var_decl :
        Ptree_helpers.F.state ->
        Why3.Ptree.pty -> string -> Why3.Ptree.ident * Ptree_helpers.F.state
      val begin_let :
        Ptree_helpers.F.state ->
        ?ghost:bool ->
        ?diverges:bool ->
        ?ret_type:Why3.Ptree.pty ->
        string -> Why3.Ptree.binder list -> Ptree_helpers.F.state
      val add_pre :
        Ptree_helpers.F.state -> Why3.Ptree.term -> Ptree_helpers.F.state
      val add_writes :
        Ptree_helpers.F.state ->
        Why3.Ptree.term list -> Ptree_helpers.F.state
      val add_post :
        Ptree_helpers.F.state -> Why3.Ptree.term -> Ptree_helpers.F.state
      val add_body :
        Ptree_helpers.F.state -> Why3.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 -> Why3.Ptree.mlw_file
    end
  module I :
    sig
      val begin_module :
        ?loc:Why3.Loc.position -> ?intf:Why3.Ptree.qualid -> string -> unit
      val use : ?loc:Why3.Loc.position -> import:bool -> string list -> unit
      val add_prop :
        Why3.Decl.prop_kind ->
        ?loc:Why3.Loc.position -> string -> Why3.Ptree.term -> unit
      val add_global_var_decl : Why3.Ptree.pty -> string -> Why3.Ptree.ident
      val begin_let :
        ?ghost:bool ->
        ?diverges:bool ->
        ?ret_type:Why3.Ptree.pty -> string -> Why3.Ptree.binder list -> unit
      val add_pre : Why3.Ptree.term -> unit
      val add_writes : Why3.Ptree.term list -> unit
      val add_post : Why3.Ptree.term -> unit
      val add_body : Why3.Ptree.expr -> unit
      val end_module : unit -> unit
      val get_mlw_file : unit -> Why3.Ptree.mlw_file
    end
end