Class `Make.engine`Source

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_trigger : (T.var, T.Fun.t) Qed.Engine.ftrigger 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

Install