def Lean.Elab.Term.elabCoe : TermElab

Equations

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

def Lean.Elab.Term.elabCoeFunNotation : TermElab

Equations

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

def Lean.Elab.Term.elabCoeSortNotation : TermElab

Equations

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

def Lean.Elab.Term.elabAnonymousCtor : TermElab

Equations

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

def Lean.Elab.Term.elabBorrowed : TermElab

Equations

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

def Lean.Elab.Term.expandShow : Macro

Equations

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

def Lean.Elab.Term.elabShow : TermElab

Equations

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

def Lean.Elab.Term.expandHave : Macro

Equations

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

def Lean.Elab.Term.expandSuffices : Macro

Equations

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

def Lean.Elab.Term.elabLeadingParserMacro : TermElab

Equations

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

def Lean.Elab.Term.elabTrailingParserMacro : TermElab

Equations

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

def Lean.Elab.Term.elabPanic : TermElab

Equations

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

def Lean.Elab.Term.expandUnreachable : Macro

Equations

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

def Lean.Elab.Term.expandAssert : Macro

Equations

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

opaque Lean.Elab.Term.debugAssertions : Lean.Option Bool

def Lean.Elab.Term.elabDebugAssert : TermElab

Equations

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

def Lean.Elab.Term.expandDbgTrace : Macro

Equations

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

def Lean.Elab.Term.elabSorry : TermElab

Equations

• Lean.Elab.Term.elabSorry x✝ expectedType? = do let type ← expectedType?.getDM (liftM Lean.Meta.mkFreshTypeMVar) liftM (Lean.Meta.mkLabeledSorry type false true)

def Lean.Elab.Term.mkPairs (elems : Array Term) : MacroM 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 (elems.size - 1) elems.back!

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

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

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

Equations

• Lean.Elab.Term.mkPPairs elems = Lean.Elab.Term.mkPPairs.loop elems (elems.size - 1) elems.back!

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

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

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

Equations

• Lean.Elab.Term.mkMPairs elems = Lean.Elab.Term.mkMPairs.loop elems (elems.size - 1) elems.back!

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

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

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

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

• · + 1 => fun x => x + 1
• f · · b => fun x1 x2 => f x1 x2 b

Equations

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

partial def Lean.Elab.Term.expandCDot?.go : Syntax → StateT (Array Ident) MacroM 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 it in the extra state, and return it. Otherwise, we just return stx.

def Lean.Elab.Term.elabCDotFunctionAlias? (stx : Term) : TermElabM (Option 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 : Term) : MacroM (Option Term)

Equations

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

def Lean.Elab.Term.expandParen : Macro

Equations

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

def Lean.Elab.Term.expandTuple : Macro

Equations

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

def Lean.Elab.Term.expandTypeAscription : Macro

Equations

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

def Lean.Elab.Term.elabTypeAscription : TermElab

Equations

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

def Lean.Elab.Term.elabSubst : TermElab

Equations

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

def Lean.Elab.Term.elabStateRefT : TermElab

Equations

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

def Lean.Elab.Term.elabNoindex : TermElab

Equations

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

def Lean.Elab.Term.elabUnsafe : TermElab

Equations

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

def Lean.Elab.Term.elabRunElab : TermElab

Elaborator for by_elab.

Equations

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

def Lean.Elab.Term.elabHaveI : TermElab

Equations

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

def Lean.Elab.Term.elabLetI : TermElab

Equations

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