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.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!

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!

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!

def Lean.Elab.Term.isCDotBinderKind (k : SyntaxNodeKind) : Bool

Equations

• Lean.Elab.Term.isCDotBinderKind k = (k == `Lean.Parser.Term.paren || k == `Lean.Parser.Term.typeAscription || k == `Lean.Parser.Term.tuple)

def Lean.Elab.Term.isCDotForInfo (s : Syntax) (hygieneInfo? : Option Name) : Bool

Returns whether or not this cdot is for the given HygieneInfo name; if no hygiene info is given, then matches any cdot, no matter its hygieneInfo.

Equations

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

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

Returns true if the given expression contains a cdot for the given HygieneInfo name. If no HygieneInfo name is given, then returns true if there is any cdot. The search is delimited by cdot binders (any syntax satisfying isCDotBinderKind).

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

If the term contains any cdots that match the given HygieneInfo name (see isCDotForInfo), then returns some with the expanded syntax, otherwise returns 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.

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.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.