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

- id : Syntax
- type : Syntax
- bi : BinderInfo

Instances For

source
partial def Lean.Elab.Term.quoteAutoTactic :
Syntax → CoreM Expr
source
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.

Instances For

source
def Lean.Elab.Term.failedToInferBinderTypeErrorName :
Name

The error name for "failed to infer binder type" errors.

We cannot use `logNamedError` here because the error is logged later, after attempting to synthesize metavariables, in `logUnassignedUsingErrorInfos`.

Equations

- Lean.Elab.Term.failedToInferBinderTypeErrorName = `lean.inferBinderTypeFailed

Instances For

source
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

Instances For

source
opaque Lean.Elab.Term.checkBinderAnnotations :
Lean.Option Bool
source
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)

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

source
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 #[]

Instances For

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

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

Instances For

source
partial def Lean.Elab.Term.FunBinders.elabFunBindersAux (binders : Array Syntax) (i : Nat) (s : State) :
TermElabM State
source
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.

Instances For

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

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

Instances For

source
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

Instances For

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

Instances For

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

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

Instances For

source
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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
structure Lean.Elab.Term.LetConfig :
Type

Configuration for `let` elaboration.

- nondep : Bool

  Elaborate as a nondependent `let` (a `have`).

- usedOnly : Bool

  Eliminate the `let` if it is unused by the body.

- zeta : Bool

  Zeta reduces (inlines) the `let`.

- postponeValue : Bool

  Postpone elaboration of the value until after the body is elaborated.

- generalize : Bool

  Generalize the value from the expected type when elaborating the body.

- eq? : Option Ident

  For `let x := v; b`, adds `eq : x = v` to the context.

Instances For

source
def Lean.Elab.Term.LetConfig.setFrom (config : LetConfig) (key : Syntax) (val : Bool) :
LetConfig
Equations

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

Instances For

source
def Lean.Elab.Term.mkLetConfig (letConfig : Syntax) (initConfig : LetConfig) :
TermElabM LetConfig

Interprets a `Parser.Term.letConfig`.

Equations

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

Instances For

source
def Lean.Elab.Term.elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx valStx body : Syntax) (expectedType? : Option Expr) (config : LetConfig) :
TermElabM Expr

The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`. If `config.postponeValue == true`, then we use the order `binders`, `typeStx`, `body`, and `valStx`. If `config.generalize == true`, then the value is abstracted from the expected type when elaborating the body.

Equations

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

Instances For

source
structure Lean.Elab.Term.LetIdDeclView :
Type

- id : Syntax
- binders : Array Syntax
- type : Syntax
- value : Syntax

Instances For

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

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

Instances For

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

Instances For

source
def Lean.Elab.Term.elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (initConfig : LetConfig) :
TermElabM Expr
Equations

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

Instances For

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

- Lean.Elab.Term.elabLetDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? { }

Instances For

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

- Lean.Elab.Term.elabHaveDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? { nondep := true }

Instances For

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

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

Instances For

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

- Lean.Elab.Term.elabLetDelayedDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? { postponeValue := true }

Instances For

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

- Lean.Elab.Term.elabLetTmpDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? { usedOnly := true }

Instances For

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

- Lean.Elab.Term.elabLetIDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? { zeta := true }

Instances For

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

- Lean.Elab.Term.elabHaveIDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? { nondep := true, zeta := true }

Instances For