Wp.Pcond
val pretty : Conditions.sequent Qed.Plib.printer
val dump : Conditions.bundle Qed.Plib.printer
val dump_bundle :
?clause:string ->
?goal:Lang.F.pred ->
Conditions.bundle Qed.Plib.printer
val dump_sequence :
?clause:string ->
?goal:Lang.F.pred ->
Conditions.sequence Qed.Plib.printer
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
Sequent Printer Engine. Uses the following CSS
:
"wp:clause"
for all clause keywords"wp:comment"
for descriptions"wp:warning"
for warnings"wp:property"
for propertiesclass engine : Plang.engine -> object ... end
class state : object ... end