Entailment-shaped goal decomposition: unfolding Triple.of_entails_wp, splitting PostCond.entails/ExceptConds.entails, and the multi-phase solveSPredEntails that drives H ⊢ₛ T to either a closed goal or a residual.

def Lean.Elab.Tactic.Do.Internal.VCGen.tripleOfWP (goal : MVarId) : VCGenM MVarId

Unfold ⦃P⦄ x ⦃Q⦄ into P ⊢ₛ wp⟦x⟧ Q by applying Tiple.of_wp, ensuring that PostShape.args ps is reduced.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.solveExceptCondsEntails (goal : MVarId) : VCGenM (Option MVarId)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.solvePostCondEntails (goal : MVarId) : VCGenM (Option (List MVarId))

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.consIntroAndSimpStep (goal : MVarId) : VCGenM (Option MVarId)

Apply SPred.entails_cons_intro to introduce one state variable, then introsSimp, then peel a leading SPred.pure (σ::σs) φ s from each side of ⊢ₛ via apply_pure_cons_entails_l/r. Returns none if no entails_cons_intro was applicable.

Performs the pure-cons cleanup at the exact iteration the state variable is introduced, so the goal stays in canonical form throughout the eta-expansion loop.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.neededStateIntro (thm : SpecAttr.SpecTheoremNew) (goal : MVarId) (excessArgs : Array Expr) : VCGenM (Option MVarId)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.solveSPredEntails (goal : MVarId) : VCGenM (Option MVarId)

Break down H ⊢ₛ T as far as possible, reporting none when no progress was made.

1. If H is pure ⌜φ₁⌝, turn the goal into h : φ₁ ⊢ ⊢ₛ T.
2. If also T is pure ⌜φ₂⌝, turn the goal into h : φ₁ ⊢ φ₂, then exit.
3. Otherwise, H or T was not pure. We continue by introducing all state variables, H s₁ ... sₙ ⊢ₛ T s₁ ... sₙ. For a monomorphic monad stack, this will an entailment on SPred []. If either H or T was pure, ⌜·⌝, state introduction preserves this.
4. Finally, turn H ⊢ₛ T into h : H.down ⊢ T.down (at SPred []).
5. If either T was pure ⌜φ₂⌝ (and H was not), we turn T.down into φ₂. (NB: If H was pure, then we have already lifted φ₁ to the local context.)

Equations

• One or more equations did not get rendered due to their size.