# Documentation

Lean.Elab.BindersUtil

Recall that

def typeSpec := leading_parser " : " >> termParser
def optType : Parser := optional typeSpec

Equations

Helper function for expandEqnsIntoMatch

Equations
def Lean.Elab.Term.expandMatchAlt (stx : Lean.TSyntax Lean.Parser.Term.matchAlt) :
Lean.MacroM (Array (Lean.TSyntax Lean.Parser.Term.matchAlt))

Expand a match alternative such as | 0 | 1 => rhs to an array containing | 0 => rhs and | 1 => rhs.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.shouldExpandMatchAlt :
Lean.TSyntax Lean.Parser.Term.matchAltBool
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.clearInMatchAlt (stx : Lean.TSyntax Lean.Parser.Term.matchAlt) (vars : ) :
Lean.TSyntax `Lean.Parser.Term.matchAlt
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.