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

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

Instances For

source
def Lean.Elab.Term.elabCoeFunNotation :
TermElab
Equations

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

Instances For

source
def Lean.Elab.Term.elabCoeSortNotation :
TermElab
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
opaque Lean.Elab.Term.debugAssertions :
Lean.Option Bool
source
def Lean.Elab.Term.elabDebugAssert :
TermElab
Equations

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

Instances For

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

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

Instances For

source
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)

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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)

Instances For

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

Instances For

source
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`).

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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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)

Instances For

source
def Lean.Elab.Term.elabUnsafe :
TermElab
Equations

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

Instances For

source
def Lean.Elab.Term.elabRunElab :
TermElab

Elaborator for `by_elab`.

Equations

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

Instances For