sig   type scope = Qed.Engine.scope   module Env :     sig       type t       val create : unit -> t       val copy : t -> t       val clear : t -> unit       val used : t -> string -> bool       val fresh : t -> ?suggest:bool -> string -> string       val define : t -> string -> Lang.F.term -> unit       val unfold : t -> Lang.F.term -> unit       val shared : t -> Lang.F.term -> bool       val shareable : t -> Lang.F.term -> bool       val lookup : t -> Lang.F.term -> Qed.Engine.scope     end   type pool   val pool : unit -> Plang.pool   val xmark_e : Plang.pool -> (Lang.F.var -> unit) -> Lang.F.term -> unit   val xmark_p : Plang.pool -> (Lang.F.var -> unit) -> Lang.F.pred -> unit   val xmark : Plang.pool -> Lang.F.Vars.t   class engine :     object       method basename : string -> string       method bind : Lang.F.var -> string       method callstyle : Qed.Engine.callstyle       method datatype : Lang.ADT.t -> string       method datatypename : string -> string       method e_false : Qed.Engine.cmode -> string       method e_true : Qed.Engine.cmode -> string       method env : Env.t       method field : Lang.Field.t -> string       method fieldname : string -> string       method find : Lang.F.var -> string       method funname : string -> string       method global : (unit -> unit) -> unit       method infoprover : 'Lang.infoprover -> 'a       method is_atomic : Lang.F.term -> bool       method is_shareable : Lang.F.term -> bool       method link : Lang.Fun.t -> Qed.Engine.link       method local : (unit -> unit) -> unit       method lookup : Lang.F.term -> Qed.Engine.scope       method marks : Plang.Env.t * Lang.F.marks       method mode : Qed.Engine.mode       method op_add : Qed.Engine.amode -> Qed.Engine.op       method op_and : Qed.Engine.cmode -> Qed.Engine.op       method op_div : Qed.Engine.amode -> Qed.Engine.op       method op_eq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op       method op_equal : Qed.Engine.cmode -> Qed.Engine.op       method op_equiv : Qed.Engine.cmode -> Qed.Engine.op       method op_imply : Qed.Engine.cmode -> Qed.Engine.op       method op_leq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op       method op_lt : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op       method op_minus : Qed.Engine.amode -> Qed.Engine.op       method op_mod : Qed.Engine.amode -> Qed.Engine.op       method op_mul : Qed.Engine.amode -> Qed.Engine.op       method op_neq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op       method op_not : Qed.Engine.cmode -> Qed.Engine.op       method op_noteq : Qed.Engine.cmode -> Qed.Engine.op       method op_or : Qed.Engine.cmode -> Qed.Engine.op       method op_real_of_int : Qed.Engine.op       method op_scope : Qed.Engine.amode -> string option       method op_spaced : string -> bool       method op_sub : Qed.Engine.amode -> Qed.Engine.op       method pp_apply :         Qed.Engine.cmode -> Lang.F.term -> Lang.F.term list Qed.Plib.printer       method pp_array : Lang.F.tau Qed.Plib.printer       method pp_array_get :         Format.formatter -> Lang.F.term -> Lang.F.term -> unit       method pp_array_set :         Format.formatter -> Lang.F.term -> Lang.F.term -> Lang.F.term -> unit       method pp_atom : Lang.F.term Qed.Plib.printer       method pp_conditional :         Format.formatter -> Lang.F.term -> Lang.F.term -> Lang.F.term -> unit       method pp_cst : Qed.Numbers.cst Qed.Plib.printer       method pp_datatype : Lang.F.ADT.t -> Lang.F.tau list Qed.Plib.printer       method pp_def_fields :         (Lang.F.Field.t * Lang.F.term) list Qed.Plib.printer       method pp_equal : Lang.F.term Qed.Plib.printer2       method pp_exists : Lang.F.tau -> string list Qed.Plib.printer       method pp_expr : Lang.F.tau -> Lang.F.term Qed.Plib.printer       method pp_farray : Lang.F.tau Qed.Plib.printer2       method pp_flow : Lang.F.term Qed.Plib.printer       method pp_forall : Lang.F.tau -> string list Qed.Plib.printer       method pp_fun :         Qed.Engine.cmode -> Lang.F.Fun.t -> Lang.F.term list Qed.Plib.printer       method pp_get_field :         Format.formatter -> Lang.F.term -> Lang.F.Field.t -> unit       method pp_imply :         Format.formatter -> Lang.F.term list -> Lang.F.term -> unit       method pp_int : Qed.Engine.amode -> Lang.F.Z.t Qed.Plib.printer       method pp_lambda : (string * Lang.F.tau) list Qed.Plib.printer       method pp_let :         Format.formatter -> Qed.Engine.pmode -> string -> Lang.F.term -> unit       method pp_not : Lang.F.term Qed.Plib.printer       method pp_noteq : Lang.F.term Qed.Plib.printer2       method pp_pred : Format.formatter -> Lang.F.pred -> unit       method pp_prop : Lang.F.term Qed.Plib.printer       method pp_real : Qed.R.t Qed.Plib.printer       method pp_sort : Lang.F.term Qed.Plib.printer       method pp_subtau : Lang.F.tau Qed.Plib.printer       method pp_tau : Lang.F.tau Qed.Plib.printer       method pp_term : Lang.F.term Qed.Plib.printer       method pp_times : Format.formatter -> Lang.F.Z.t -> Lang.F.term -> unit       method pp_tvar : int Qed.Plib.printer       method pp_var : string Qed.Plib.printer       method scope : Env.t -> (unit -> unit) -> unit       method t_atomic : Lang.F.tau -> bool       method t_bool : string       method t_int : string       method t_prop : string       method t_real : string       method with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit     end end