def
Std.Internal.Do.assertGadget
{m : Type u → Type v}
{Pred EPred : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
(name : Lean.Name)
(as : Pred)
:
m PUnit
A no-op computation used as a verification gadget to inject assertions into the program.
The name parameter is used by VCGen to name the introduced hypothesis. The as parameter
is the assertion to be checked. At runtime, assertGadget is simply pure ⟨⟩.
Equations
- Std.Internal.Do.assertGadget name as = pure PUnit.unit
Instances For
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}
(name : Lean.Name)
(as : Pred)
[Lean.Order.Frame Pred]
:
Triple (Lean.Order.meet as (Lean.Order.himp as (post PUnit.unit))) (Do.assertGadget name 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.