module Pcond: sig
.. end
All-in-one printers
val dump : Wp.Conditions.bundle Qed.Plib.printer
val bundle : ?clause:string -> Wp.Conditions.bundle Qed.Plib.printer
val sequence : ?clause:string -> Wp.Conditions.sequence Qed.Plib.printer
val pretty : Wp.Conditions.sequent Qed.Plib.printer
Low-level API
type
env = Wp.Plang.Env.t
val alloc_hyp : Wp.Plang.pool -> (Wp.Lang.F.var -> unit) -> Wp.Conditions.sequence -> unit
val alloc_seq : Wp.Plang.pool -> (Wp.Lang.F.var -> unit) -> Wp.Conditions.sequent -> unit
Sequent Printer Engine. Uses the following CSS
:
"wp:clause"
for all clause keywords
"wp:comment"
for descriptions
"wp:warning"
for warnings
"wp:property"
for properties
class engine : #Wp.Plang.engine ->
object
.. end
class state :
object
.. end
class sequence : #state ->
object
.. end