structure Lean.Elab.Term.BinderView : Type

Auxiliary datatype for elaborating binders.

• ref : Syntax

  Position information provider for the Info Tree. We currently do not track binder "macro expansion" steps in the info tree. For example, suppose we expand a _ into a fresh identifier. The fresh identifier has synthetic position since it was not written by the user, and we would not get hover information for the _ because we also don't have this macro expansion step stored in the info tree. Thus, we store the original Syntax in ref, and use it when storing the binder information in the info tree.

  Potential better solution: add a binder syntax category, an extensible elabBinder (like we have elabTerm), and perform all macro expansion steps at elabBinder and record them in the infro tree.

• id : Syntax
• type : Syntax
• bi : BinderInfo

def Lean.Elab.Term.kindOfBinderName (binderName : Name) : LocalDeclKind

Determines the local declaration kind depending on the variable name.

The __x in let __x := 42; body gets kind .implDetail.

Equations

• Lean.Elab.Term.kindOfBinderName binderName = if binderName.isImplementationDetail = true then Lean.LocalDeclKind.implDetail else Lean.LocalDeclKind.default

partial def Lean.Elab.Term.quoteAutoTactic : Syntax → CoreM Expr

def Lean.Elab.Term.declareTacticSyntax (tactic : Syntax) (name? : Option Name := none) : TermElabM Name

Adds a declaration whose value is a Syntax expression representing tactic. If name? is provided, it is used for the declaration name, and otherwise a fresh name is generated. Returns the declaration name.

Equations

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

def Lean.Elab.Term.addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit

Equations

• Lean.Elab.Term.addLocalVarInfo stx fvar = Lean.Elab.Term.addTermInfo' stx fvar none none Lean.Name.anonymous true

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

def Lean.Elab.Term.elabBindersEx {α : Type} (binders : Array Syntax) (k : Array (Syntax × Expr) → TermElabM α) : TermElabM α

Like elabBinders, but also pass syntax node per binder. elabBinders(Ex) automatically adds binder info nodes for the produced fvars, but storing the syntax nodes might be necessary when later adding the same binders back to the local context so that info nodes can manually be added for the new fvars; see MutualDef for an example.

Equations

• Lean.Elab.Term.elabBindersEx binders k = Lean.Elab.Term.universeConstraintsCheckpoint (if binders.isEmpty = true then k #[] else Lean.Elab.Term.elabBindersAux✝ binders k)

def Lean.Elab.Term.elabBinders {α : Type} (binders : Array Syntax) (k : Array Expr → TermElabM α) : TermElabM α

Elaborate the given binders (i.e., Syntax objects for bracketedBinder), update the local context, set of local instances, reset instance cache (if needed), and then execute k with the updated context. The local context will only be included inside k.

For example, suppose you have binders [(a : α), (b : β a)], then the elaborator will create two new free variables a and b, push these to the context and pass to k #[a,b].

Equations

• Lean.Elab.Term.elabBinders binders k = Lean.Elab.Term.elabBindersEx binders fun (fvars : Array (Lean.Syntax × Lean.Expr)) => k (Array.map (fun (x : Lean.Syntax × Lean.Expr) => x.snd) fvars)

def Lean.Elab.Term.elabBinder {α : Type} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α

Same as elabBinder with a single binder.

Equations

• Lean.Elab.Term.elabBinder binder x = Lean.Elab.Term.elabBinders #[binder] fun (fvars : Array Lean.Expr) => x fvars[0]!

def Lean.Elab.Term.expandSimpleBinderWithType (type : Term) (binder : Syntax) : MacroM Syntax

If binder is a _ or an identifier, return a bracketedBinder using type otherwise throw an exception.

Equations

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

def Lean.Elab.Term.expandForall : Macro

Equations

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

def Lean.Elab.Term.elabForall : TermElab

Equations

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

def Lean.Elab.Term.precheckArrow : Quotation.Precheck

Equations

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

def Lean.Elab.Term.elabArrow : TermElab

Equations

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

def Lean.Elab.Term.elabDepArrow : TermElab

The dependent arrow. (x : α) → β is equivalent to ∀ x : α, β, but we usually reserve the latter for propositions. Also written as Π x : α, β (the "Pi-type") in the literature.

Equations

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

def Lean.Elab.Term.expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (Array Syntax × Syntax × Bool)

Auxiliary function for expanding fun notation binders. Recall that fun parser is defined as

def funBinder : Parser := implicitBinder <|> instBinder <|> termParser maxPrec
leading_parser unicodeSymbol "λ" "fun" >> many1 funBinder >> "=>" >> termParser

to allow notation such as fun (a, b) => a + b, where (a, b) should be treated as a pattern. The result is a pair (explicitBinders, newBody), where explicitBinders is syntax of the form

`(` ident `:` term `)`

which can be elaborated using elabBinders, and newBody is the updated body syntax. We update the body syntax when expanding the pattern notation. Example: fun (a, b) => a + b expands into fun _a_1 => match _a_1 with | (a, b) => a + b. See local function processAsPattern at expandFunBindersAux.

The resulting Bool is true if a pattern was found. We use it "mark" a macro expansion.

Equations

• Lean.Elab.Term.expandFunBinders binders body = Lean.Elab.Term.expandFunBinders.loop binders body 0 #[]

partial def Lean.Elab.Term.expandFunBinders.loop (binders : Array Syntax) (body : Syntax) (i : Nat) (newBinders : Array Syntax) : MacroM (Array Syntax × Syntax × Bool)

structure Lean.Elab.Term.FunBinders.State : Type

• fvars : Array Expr
• lctx : LocalContext
• localInsts : LocalInstances
• expectedType? : Option Expr

partial def Lean.Elab.Term.FunBinders.elabFunBindersAux (binders : Array Syntax) (i : Nat) (s : State) : TermElabM State

def Lean.Elab.Term.elabFunBinders {α : Type} (binders : Array Syntax) (expectedType? : Option Expr) (x : Array Expr → Option Expr → TermElabM α) : TermElabM α

Equations

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

def Lean.Elab.Term.expandWhereDecls (whereDecls body : Syntax) : MacroM Syntax

Equations

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

def Lean.Elab.Term.expandWhereDeclsOpt (whereDeclsOpt body : Syntax) : MacroM Syntax

Equations

• Lean.Elab.Term.expandWhereDeclsOpt whereDeclsOpt body = if whereDeclsOpt.isNone = true then pure body else Lean.Elab.Term.expandWhereDecls whereDeclsOpt[0] body

def Lean.Elab.Term.expandMatchAltsIntoMatch (ref matchAlts : Syntax) (useExplicit : Bool := true) : MacroM Syntax

Expand matchAlts syntax into a full match-expression. Example:

| 0, true => alt_1
| i, _    => alt_2

expands into (for tactic == false)

fun x_1 x_2 =>
match @x_1, @x_2 with
| 0, true => alt_1
| i, _    => alt_2

and (for tactic == true)

intro x_1; intro x_2;
match @x_1, @x_2 with
| 0, true => alt_1
| i, _    => alt_2

If useExplicit = true, we add a @ before fun to disable implicit lambdas. We disable them when processing let and let rec declarations to make sure the behavior is consistent with top-level declarations where we can write

def f : {α : Type} → α → α
  | _, a => a

We use useExplicit = false when we are elaborating the fun | ... => ... | ... notation. See issue #1132. If @fun is used with this notation, the we set useExplicit = true. We also use useExplicit = false when processing instance ... where notation declarations. The motivation is to have compact declarations such as

instance [Alternative m] : MonadLiftT Option m where
monadLift -- We don't want to provide the implicit arguments of `monadLift` here. One should use `monadLift := @fun ...` if they want to provide them.
  | some a => pure a
  | none => failure

Remark: we add @ at discriminants to make sure we don't consume implicit arguments, and to make the behavior consistent with fun. Example:

inductive T : Type 1 :=
| mkT : (forall {a : Type}, a -> a) -> T

def makeT (f : forall {a : Type}, a -> a) : T :=
  mkT f

def makeT' : (forall {a : Type}, a -> a) -> T
| f => mkT f

The two definitions should be elaborated without errors and be equivalent.

Equations

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

def Lean.Elab.Term.expandMatchAltsIntoMatchTactic (ref matchAlts : Syntax) : MacroM Syntax

Equations

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

def Lean.Elab.Term.expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) (expectedType : Expr) : TermElabM Syntax

Similar to expandMatchAltsIntoMatch, but supports an optional where clause.

Expand matchAltsWhereDecls into let rec + match-expression. Example

| 0, true => ... f 0 ...
| i, _    => ... f i + g i ...
where
  f x := g x + 1

  g : Nat → Nat
    | 0   => 1
    | x+1 => f x

expands into

fux x_1 x_2 =>
  let rec
    f x := g x + 1,
    g : Nat → Nat
      | 0   => 1
      | x+1 => f x
  match x_1, x_2 with
  | 0, true => ... f 0 ...
  | i, _    => ... f i + g i ...

Equations

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

def Lean.Elab.Term.expandMatchAltsWhereDecls.loop (expectedType : Expr) (matchAlts whereDeclsOpt : Syntax) (i : Nat) (discrs : Array Syntax) : TermElabM Syntax

Equations

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

def Lean.Elab.Term.expandFun : Macro

Equations

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

def Lean.Elab.Term.expandExplicitFun : Macro

Equations

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

def Lean.Elab.Term.precheckFun : Quotation.Precheck

Equations

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

def Lean.Elab.Term.elabFun : TermElab

Equations

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

def Lean.Elab.Term.elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx valStx body : Syntax) (expectedType? : Option Expr) (useLetExpr elabBodyFirst usedLetOnly : Bool) : TermElabM Expr

If useLetExpr is true, then a kernel let-expression let x : type := val; body is created. Otherwise, we create a term of the form letFun val (fun (x : type) => body)

The default elaboration order is binders, typeStx, valStx, and body. If elabBodyFirst == true, then we use the order binders, typeStx, body, and valStx.

Equations

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

structure Lean.Elab.Term.LetIdDeclView : Type

• id : Syntax
• binders : Array Syntax
• type : Syntax
• value : Syntax

def Lean.Elab.Term.mkLetIdDeclView (letIdDecl : Syntax) : LetIdDeclView

Equations

• Lean.Elab.Term.mkLetIdDeclView letIdDecl = { id := letIdDecl[0], binders := letIdDecl[1].getArgs, type := Lean.Elab.Term.expandOptType letIdDecl[0] letIdDecl[2], value := letIdDecl[4] }

def Lean.Elab.Term.expandLetEqnsDecl (letDecl : Syntax) (useExplicit : Bool := true) : MacroM Syntax

Equations

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

def Lean.Elab.Term.elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr elabBodyFirst usedLetOnly : Bool) : TermElabM Expr

Equations

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

def Lean.Elab.Term.elabLetDecl : TermElab

Equations

• Lean.Elab.Term.elabLetDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? true false false

def Lean.Elab.Term.elabLetFunDecl : TermElab

Equations

• Lean.Elab.Term.elabLetFunDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? false false false

def Lean.Elab.Term.elabLetDelayedDecl : TermElab

Equations

• Lean.Elab.Term.elabLetDelayedDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? true true false

def Lean.Elab.Term.elabLetTmpDecl : TermElab

Equations

• Lean.Elab.Term.elabLetTmpDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? true false true