class engine :#Plang.engine ->
object
..end
method name : env -> Lang.F.term -> string
Generate a name for marked term
method mark : Lang.F.marks -> Conditions.step -> unit
method pp_clause : string Qed.Plib.printer
"@{<wp:clause>...}"
method pp_stmt : string Qed.Plib.printer
"@{<wp:stmt>...}"
method pp_comment : string Qed.Plib.printer
"@{<wp:comment>(* ... *)}"
method pp_property : Property.t Qed.Plib.printer
"@{<wp:property>(* ... *)}"
method pp_warning : Warning.t Qed.Plib.printer
"@{<wp:warning>Warning}..."
method pp_name : string Qed.Plib.printer
Format.pp_print_string
method pp_core : Lang.F.term Qed.Plib.printer
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_block : clause:string -> Conditions.sequence Qed.Plib.printer
method pp_goal : Lang.F.pred Qed.Plib.printer
method pp_step : Conditions.step Qed.Plib.printer
method pp_sequence : clause:string -> Conditions.sequence Qed.Plib.printer
method pp_sequent : Conditions.sequent Qed.Plib.printer
method pp_esequent : env -> Conditions.sequent Qed.Plib.printer