def Lean.Elab.Term.elabCoe : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabAnonymousCtor : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabBorrowed : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.expandShow : Lean.Macro

Equations

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

def Lean.Elab.Term.elabShow : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.expandHave : Lean.Macro

Equations

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

def Lean.Elab.Term.expandSuffices : Lean.Macro

Equations

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

def Lean.Elab.Term.elabLeadingParserMacro : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabTrailingParserMacro : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabPanic : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.expandUnreachable : Lean.Macro

Equations

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

def Lean.Elab.Term.expandAssert : Lean.Macro

Equations

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

def Lean.Elab.Term.expandDbgTrace : Lean.Macro

Equations

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

def Lean.Elab.Term.elabSorry : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.mkPairs (elems : Array Lean.Term) : Lean.MacroM Lean.Term

Return syntax Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))

Equations

• Lean.Elab.Term.mkPairs elems = Lean.Elab.Term.mkPairs.loop elems (Array.size elems - 1) (Array.back elems)

partial def Lean.Elab.Term.mkPairs.loop (elems : Array Lean.Term) (i : Nat) (acc : Lean.Term) : Lean.MacroM Lean.Term

partial def Lean.Elab.Term.hasCDot : Lean.Syntax → Bool

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

Return some if succeeded expanding · notation occurring in the given syntax. Otherwise, return none. Examples:

• · + 1 => fun _a_1 => _a_1 + 1
• f · · b => fun _a_1 _a_2 => f _a_1 _a_2 b

Equations

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

partial def Lean.Elab.Term.expandCDot?.go : Lean.Syntax → StateT (Array Lean.Ident) Lean.MacroM Lean.Syntax

Auxiliary function for expanding the · notation. The extra state Array Syntax contains the new binder names. If stx is a ·, we create a fresh identifier, store in the extra state, and return it. Otherwise, we just return stx.

def Lean.Elab.Term.elabCDotFunctionAlias? (stx : Lean.Term) : Lean.Elab.TermElabM (Option Lean.Expr)

Helper method for elaborating terms such as (.+.) where a constant name is expected. This method is usually used to implement tactics that take function names as arguments (e.g., simp).

Equations

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

def Lean.Elab.Term.elabCDotFunctionAlias?.expandCDotArg? (stx : Lean.Term) : Lean.MacroM (Option Lean.Term)

Equations

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

def Lean.Elab.Term.expandParen : Lean.Macro

Equations

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

def Lean.Elab.Term.expandTuple : Lean.Macro

Equations

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

def Lean.Elab.Term.expandTypeAscription : Lean.Macro

Equations

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

def Lean.Elab.Term.elabTypeAscription : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabSubst : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabStateRefT : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabNoindex : Lean.Elab.Term.TermElab

Equations

• Lean.Elab.Term.elabNoindex stx expectedType? = do let e ← Lean.Elab.Term.elabTerm stx[1] expectedType? true true pure (Lean.Meta.DiscrTree.mkNoindexAnnotation e)