Module CfgCompiler.ESource

Relocatable effect (a predicate that depend on two states).

Sourcetype t
Sourceval pretty : Format.formatter -> t -> unit

Bundle an equation with the sigma sequence that created it

Sourceval get : t -> Lang.F.pred
Sourceval reads : t -> Sigma.domain
Sourceval writes : t -> Sigma.domain

as defined by S.writes

Sourceval relocate : Sigma.sigma Memory.sequence -> t -> t