Module Pcond

module Pcond: sig .. end

All-in-one printers

val dump : Conditions.bundle Qed.Plib.printer

val bundle : ?clause:string -> Conditions.bundle Qed.Plib.printer

val sequence : ?clause:string -> Conditions.sequence Qed.Plib.printer

val pretty : Conditions.sequent Qed.Plib.printer

Low-level API

type env = Plang.Env.t 

val alloc_hyp : Plang.pool -> (Lang.F.var -> unit) -> Conditions.sequence -> unit

val alloc_seq : Plang.pool -> (Lang.F.var -> unit) -> Conditions.sequent -> unit

• "wp:clause" for all clause keywords
• "wp:comment" for descriptions
• "wp:warning" for warnings
• "wp:property" for properties
• "wp:"

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

class state : object .. end

class sequence : #state -> object .. end