Helpers for decomposing exception-postcondition (EPost) goals: reducing an EPost.Cons.head projection in the RHS of an entailment to the underlying component. The concrete case (epost⟨…⟩) is handled by mkEPostAtIndex/peelEPostTailChain; the ⊥ case is handled by replaceEPostHeadBot?, which rewrites pre ⊑ ⊥.head x₁ … xₙ to pre ⊑ ⊥.

def Lean.Elab.Tactic.Do.Internal.VCGen.mkEPostAtIndex (target : Expr) (index : Nat) : Meta.Sym.SymM (Option Expr)

Get the index-th component from an EPost target.

Equations

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

partial def Lean.Elab.Tactic.Do.Internal.VCGen.peelEPostTailChain (curr : Expr) (idx : Nat := 0) : Expr × Nat

Peel a chain of .tail projections, returning the base EPost and the number of tails.

def Lean.Elab.Tactic.Do.Internal.VCGen.replaceEPostHeadBot? (goal : MVarId) (target head : Expr) (args : Array Expr) : Meta.Sym.SymM (Option MVarId)

When the exception postcondition is ⊥, the RHS of a pre ⊑ EPost.Cons.head ⊥ x₁ … xₙ goal is propositionally—but not definitionally—equal to ⊥. This rewrites the goal to pre ⊑ ⊥, constructing the equality proof from EPost.Cons.head_bot (for the head projection) and bot_apply (for each excess argument).

The proof term is built directly with mkApp/mkConst and instances extracted from the existing goal, avoiding mkAppM/instance synthesis (which is both expensive and unable to unify max-of- universe-variable instance levels in the abstract-monad setting).

head/args come from rhs.withApp, where rhs = EPost.Cons.head eh et ⊥ x₁ … xₙ, and target is the full pre ⊑ rhs entailment. Returns the rewritten goal, or none if args[2] is not ⊥ or the lattice instances are not in the expected shape (the caller then falls through).

Equations

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