Documentation

Lean.Elab.BindersUtil

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

Equations

Lean.Elab.Term.expandOptType ref optType = if Lean.Syntax.isNone optType = true then Lean.mkHole ref else Lean.Syntax.getOp (Lean.Syntax.getOp optType 0) 1

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

Equations

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

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.matchAlt → Bool

Equations

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

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

Lean.MacroM (Option Lean.Syntax)

Equations

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