module E:sig
..end
Relocatable effect (a predicate that depend on two states).
type
t
val pretty : Stdlib.Format.formatter -> t -> unit
val create : S.t Wp.Sigs.sequence -> Wp.Lang.F.pred -> t
Bundle an equation with the sigma sequence that created it
val get : t -> Wp.Lang.F.pred
val reads : t -> S.domain
val writes : t -> S.domain
as defined by S.writes
val relocate : S.t Wp.Sigs.sequence -> t -> t