Class Pcond.engine

class engine : Plang.engine -> object .. end

method name : env -> Lang.F.term -> string

Printer Components

Generate a name for marked term

method mark : Lang.F.marks -> Conditions.step -> unit

Marks terms to share in step

method pp_clause : string Qed.Plib.printer

Default: "@{<wp:clause>...}"

method pp_comment : string Qed.Plib.printer

Default: "@{<wp:comment>(* ... *)}"

method pp_property : Property.t Qed.Plib.printer

Default: "@{<wp:property>(* ... *)}"

method pp_warning : Warning.t Qed.Plib.printer

Default: "@{<wp:warning>Warning}..."

method pp_name : string Qed.Plib.printer

Default: Format.pp_print_string

method pp_core : Lang.F.term Qed.Plib.printer

Default: plang#pp_sort

method pp_definition : Format.formatter -> string -> Lang.F.term -> unit

method pp_intro : step:Conditions.step ->
       clause:string -> ?dot:string -> Lang.F.pred Qed.Plib.printer

method pp_condition : step:Conditions.step -> Conditions.condition Qed.Plib.printer

method pp_step : Conditions.step Qed.Plib.printer

Assumes an "<hv>" box is opened.

method pp_sequence : clause:string -> Conditions.sequence Qed.Plib.printer

Assumes an "<hv>" box is opened.

method pp_sequent : Conditions.sequent Qed.Plib.printer

Print the sequent in global environment.

method pp_esequent : env -> Conditions.sequent Qed.Plib.printer

Print the sequent in the given environment. The environment is enrich with the shared terms.