Module Wp.Pcond

module Pcond: sig .. end

All-in-one printers

val pretty : Wp.Conditions.sequent Qed.Plib.printer

val dump : Wp.Conditions.bundle Qed.Plib.printer

val dump_bundle : ?clause:string ->
       ?goal:Wp.Lang.F.pred -> Wp.Conditions.bundle Qed.Plib.printer

val dump_sequence : ?clause:string ->
       ?goal:Wp.Lang.F.pred -> Wp.Conditions.sequence 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 seqengine : #state -> object .. end