Class Make.engineSource

inherit [Z.t, T.ADT.t, T.Field.t, T.Fun.t, T.tau, T.var, T.term, Env.t] Qed.Engine.engine
method marks : Env.t * T.marks
method op_spaced : string -> bool
method op_record : string * string
method pp_forall : T.tau -> string list Qed.Plib.printer
method pp_intros : T.tau -> string list Qed.Plib.printer
method pp_exists : T.tau -> string list Qed.Plib.printer
method pp_param : (string * T.tau) Qed.Plib.printer
method pp_declare_symbol : Qed.Engine.cmode -> T.Fun.t Qed.Plib.printer
method pp_declare_adt : Format.formatter -> T.ADT.t -> int -> unit
method pp_declare_def : Format.formatter -> T.ADT.t -> int -> T.tau -> unit
method pp_declare_sum : Format.formatter -> T.ADT.t -> int -> (T.Fun.t * T.tau list) list -> unit
method declare_type : Format.formatter -> T.ADT.t -> int -> typedef -> unit
method declare_prop : kind:string -> Format.formatter -> string -> T.var list -> trigger list list -> T.term -> unit
method declare_axiom : Format.formatter -> string -> T.var list -> trigger list list -> T.term -> unit
method declare_fixpoint : prefix:string -> Format.formatter -> T.Fun.t -> T.var list -> T.tau -> T.term -> unit
method declare_signature : Format.formatter -> T.Fun.t -> T.tau list -> T.tau -> unit
method declare_definition : Format.formatter -> T.Fun.t -> T.var list -> T.tau -> T.term -> unit