def Std.Internal.Do.assertGadget {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (as : Pred) : m PUnit

A no-op computation used as a verification gadget to inject assertions into the program.

The as parameter is the assertion to be checked. At runtime, assertGadget is simply pure ⟨⟩.

Equations

• Std.Internal.Do.assertGadget as = pure PUnit.unit

theorem Std.Internal.Do.Spec.assertGadget {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {post : PUnit → Pred} {epost : EPred} (as : Pred) [∀ (a : Pred), Lean.Order.PreservesSup (Lean.Order.meet a)] : ⦃ Lean.Order.meet as (Lean.Order.himp as (post PUnit.unit)) ⦄ Do.assertGadget as ⦃ post; epost ⦄

Specification for assertGadget: the precondition requires both the assertion as and the Heyting implication as ⇨ post ⟨⟩, ensuring the assertion holds and the postcondition follows from it.