def Lean.Elab.Term.expandOptType (ref optType : Syntax) : Syntax

Recall that

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

Equations

• Lean.Elab.Term.expandOptType ref optType = if optType.isNone = true then Lean.mkHole ref else optType[0][1]

def Lean.Elab.Term.getMatchAltsNumPatterns (matchAlts : Syntax) : Nat

Helper function for expandEqnsIntoMatch

Equations

• Lean.Elab.Term.getMatchAltsNumPatterns matchAlts = matchAlts[0][0][1][0].getSepArgs.size

def Lean.Elab.Term.expandMatchAlt (stx : TSyntax `Lean.Parser.Term.matchAlt) : MacroM (Array (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 : TSyntax `Lean.Parser.Term.matchAlt → Bool

Equations

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

def Lean.Elab.Term.expandMatchAlts? (stx : Syntax) : MacroM (Option Syntax)

Equations

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

def Lean.Elab.Term.clearInMatchAlt (stx : TSyntax `Lean.Parser.Term.matchAlt) (vars : Array Ident) : TSyntax `Lean.Parser.Term.matchAlt

Equations

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

def Lean.Elab.Term.clearInMatch (stx : Syntax) (vars : Array Ident) : MacroM Syntax

Equations

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