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.

instance Std.WP.Id.instWPConjunctive {α : Type u} (x : Id α) : WPConjunctive x

An Id program is conjunctive: its wp is evaluation at the result.

instance Std.WP.Option.instWPConjunctive {α : Type u} (x : Option α) : WPConjunctive x

An Option program is conjunctive: its wp is evaluation at the result.

instance Std.WP.Except.instWPConjunctive {ε α : Type u} (x : Except ε α) : WPConjunctive x

An Except ε program is conjunctive: its wp is evaluation at the result.

instance Std.WP.EStateM.instWPConjunctive {ε σ α : Type} (x : EStateM ε σ α) : WPConjunctive x

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} {EPosts : Type z} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] (x : StateT σ m α) [base : ∀ (s : σ), WPConjunctive (x.run s)] : WPConjunctive x

A StateT program lifts conjunctivity from its base monad.

instance Std.WP.ReaderT.instWPConjunctive {m : Type u → Type v} {ρ : Type u} {Pred : Type w} {EPosts : Type z} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] (x : ReaderT ρ m α) [base : ∀ (r : ρ), WPConjunctive (x.run r)] : WPConjunctive x

A ReaderT program lifts conjunctivity from its base monad.

instance Std.WP.OptionT.instWPConjunctive {m : Type u → Type v} {Pred : Type u} {EPosts : Type z} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] (x : OptionT m α) [base : WPConjunctive x.run] : WPConjunctive x

An OptionT program lifts conjunctivity from its base monad.

instance Std.WP.ExceptT.instWPConjunctive {m : Type u → Type v} {ε α : Type u} {Pred : Type w} {EPosts : Type z} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] (x : ExceptT ε m α) [base : WPConjunctive x.run] : WPConjunctive x

An ExceptT program lifts conjunctivity from its base monad.