sig
type t
val empty : Wp.Passive.t
val is_empty : Wp.Passive.t -> bool
val union : Wp.Passive.t -> Wp.Passive.t -> Wp.Passive.t
val bind :
fresh:Wp.Lang.F.var ->
bound:Wp.Lang.F.var -> Wp.Passive.t -> Wp.Passive.t
val join : Wp.Lang.F.var -> Wp.Lang.F.var -> Wp.Passive.t -> Wp.Passive.t
val conditions :
Wp.Passive.t -> (Wp.Lang.F.var -> bool) -> Wp.Lang.F.pred list
val apply : Wp.Passive.t -> Wp.Lang.F.pred -> Wp.Lang.F.pred
type binding =
Bind of Wp.Lang.F.var * Wp.Lang.F.var
| Join of Wp.Lang.F.var * Wp.Lang.F.var
val iter : (Wp.Passive.binding -> unit) -> Wp.Passive.t -> unit
val pretty : Format.formatter -> Wp.Passive.t -> unit
end