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

Recall that

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

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

Helper function for expandEqnsIntoMatch

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.

def Lean.Elab.Term.shouldExpandMatchAlt : Lean.TSyntax `Lean.Parser.Term.matchAlt → Bool

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

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

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