Conjunctivity of the monadic weakest preconditions #
WPConjunctive instances for the base monads and for the monad transformers. Each transformer
instance lifts conjunctivity from the programs of its base monad.
An Id program is conjunctive: its wp is evaluation at the result.
An Option program is conjunctive: its wp is evaluation at the result.
An Except ε program is conjunctive: its wp is evaluation at the result.
An EStateM program is conjunctive: its wp is evaluation at the result.
instance
Std.WP.StateT.instWPConjunctive
{m : Type u → Type v}
{σ : Type u}
{Pred : Type w}
{EPred : Type z}
{α : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
(x : StateT σ m α)
[base : ∀ (s : σ), WPConjunctive (x.run s)]
:
A StateT program lifts conjunctivity from its base monad.
instance
Std.WP.ReaderT.instWPConjunctive
{m : Type u → Type v}
{ρ : Type u}
{Pred : Type w}
{EPred : Type z}
{α : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
(x : ReaderT ρ m α)
[base : ∀ (r : ρ), WPConjunctive (x.run r)]
:
A ReaderT program lifts conjunctivity from its base monad.