Module Wp.PcondSource

All-in-one printers

Sourceval dump_bundle : ?clause:string -> ?goal:Lang.F.pred -> Conditions.bundle Qed.Plib.printer
Sourceval dump_sequence : ?clause:string -> ?goal:Lang.F.pred -> Conditions.sequence Qed.Plib.printer

Low-level API

Sourceval alloc_hyp : Plang.pool -> (Lang.F.var -> unit) -> Conditions.sequence -> unit
Sourceval alloc_seq : Plang.pool -> (Lang.F.var -> unit) -> Conditions.sequent -> unit

Sequent Printer Engine. Uses the following CSS:

Sourceclass engine : Plang.engine -> object ... end
Sourceclass state : object ... end
Sourceclass seqengine : state -> object ... end