class
Std.Internal.Do.WPConjunctive
(Prog : Type u)
(Value : outParam (Type v))
(Pred : outParam (Type w))
(EPred : outParam (Type z))
[Assertion Pred]
[Assertion EPred]
[WP Prog Value Pred EPred]
:
wp x is sub-conjunctive: a meet of postconditions maps below the wp of their meet. A
healthiness condition of the WP interpretation; it holds for the base interpretations and lifts
through the transformers.
- wp_meet_wp_le (x : Prog) (Q₁ Q₂ : Value → Pred) (E : EPred) : Lean.Order.PartialOrder.rel (Lean.Order.meet (wp x Q₁ E) (wp x Q₂ E)) (wp x (Lean.Order.meet Q₁ Q₂) E)
A meet of postconditions maps below the
wpof their meet.
Instances
Id is conjunctive: its wp is evaluation at the result.
instance
Std.Internal.Do.Option.instWPConjunctive
{α : Type u}
:
WPConjunctive (Option α) α Prop Prop
Option is conjunctive: its wp is evaluation at the result.
Except ε is conjunctive: its wp is evaluation at the result.
instance
Std.Internal.Do.EStateM.instWPConjunctive
{ε σ α : Type}
:
WPConjunctive (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop)
EStateM is conjunctive: its wp is evaluation at the result.
instance
Std.Internal.Do.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]
[WPConjunctive (m (α × σ)) (α × σ) Pred EPred]
:
WPConjunctive (StateT σ m α) α (σ → Pred) EPred
StateT lifts conjunctivity from its base monad.
instance
Std.Internal.Do.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]
[WPConjunctive (m α) α Pred EPred]
:
WPConjunctive (ReaderT ρ m α) α (ρ → Pred) EPred
ReaderT lifts conjunctivity from its base monad.
instance
Std.Internal.Do.OptionT.instWPConjunctive
{m : Type u → Type v}
{Pred : Type u}
{EPred : Type z}
{α : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[WPConjunctive (m (Option α)) (Option α) Pred EPred]
:
WPConjunctive (OptionT m α) α Pred (EPost.Cons✝ Pred EPred)
OptionT lifts conjunctivity from its base monad.
instance
Std.Internal.Do.ExceptT.instWPConjunctive
{m : Type u → Type v}
{ε α : Type u}
{Pred : Type w}
{EPred : Type z}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[WPConjunctive (m (Except ε α)) (Except ε α) Pred EPred]
:
WPConjunctive (ExceptT ε m α) α Pred (EPost.Cons✝ (ε → Pred) EPred)
ExceptT lifts conjunctivity from its base monad.