def Lean.Meta.Sym.Simp.simpArrowTelescope (simpBody : Simproc := simp) : Simproc

Simplifies a telescope of non-dependent arrows p₁ → p₂ → ... → pₙ → q by:

1. Converting to Arrow p₁ (Arrow p₂ (... (Arrow pₙ q))) (see toArrow)
2. Simplifying each pᵢ and q (see simpArrows)
3. Converting back to → form (see toForall)

Using Arrow (a definitional wrapper around →) avoids the quadratic proof growth that occurs with Expr.forallE. With forallE, each nesting level bumps de Bruijn indices in subterms, destroying sharing. For example, if each pᵢ contains a free variable x, the de Bruijn representation of x differs at each depth, preventing hash-consing from recognizing them as identical.

With Arrow, both arguments are explicit (not under binders), so subterms remain identical across nesting levels and can be shared, yielding linear-sized proofs.

Tradeoff: This function simplifies each pᵢ and q individually, but misses simplifications that depend on the arrow structure itself. For example, q → p → p won't be simplified to True (when p : Prop) because the simplifier does not have a chance to apply post methods to the intermediate arrow p → p.

Thus, this is a simproc that is meant to be used as a pre-method and marks the result as fully simplified to prevent simpArrow from being applied.

Equations

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

def Lean.Meta.Sym.Simp.simpArrow (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Sym.Simp.simpForall' (simpArrow simpBody : Simproc) (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Sym.Simp.simpForall : Simproc

Equations

• Lean.Meta.Sym.Simp.simpForall = Lean.Meta.Sym.Simp.simpForall' Lean.Meta.Sym.Simp.simpArrow Lean.Meta.Sym.Simp.simp