source
opaque Lean.Elab.Term.elabWithoutExpectedTypeAttr :
TagAttribute

Instructs the elaborator to elaborate applications of the given declaration without an expected type. This may prevent the elaborator from incorrectly inferring implicit arguments.

source
def Lean.Elab.Term.hasElabWithoutExpectedType (env : Environment) (declName : Name) :
Bool
Equations

- Lean.Elab.Term.hasElabWithoutExpectedType env declName = Lean.Elab.Term.elabWithoutExpectedTypeAttr.hasTag env declName

Instances For

source
instance Lean.Elab.Term.instToStringArg :
ToString Arg
Equations

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

source
instance Lean.Elab.Term.instToStringNamedArg :
ToString NamedArg
Equations

- Lean.Elab.Term.instToStringNamedArg = { toString := fun (s : Lean.Elab.Term.NamedArg) => "(" ++ toString s.name ++ " := " ++ toString s.val ++ ")" }

source
def Lean.Elab.Term.throwInvalidNamedArg {α : Type} (namedArg : NamedArg) (fn? : Option Name) (validNames : Array Name) :
TermElabM α
Equations

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

Instances For

source
def Lean.Elab.Term.synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) :
TermElabM Unit
Equations

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

Instances For

source
def Lean.Elab.Term.eraseNamedArg (namedArgs : List NamedArg) (binderName : Name) :
List NamedArg

Erase entry for `binderName` from `namedArgs`.

Equations

- Lean.Elab.Term.eraseNamedArg namedArgs binderName = List.filter (fun (x : Lean.Elab.Term.NamedArg) => x.name != binderName) namedArgs

Instances For

# Default application elaborator #

source
structure Lean.Elab.Term.ElabAppArgs.Context :
Type

- ellipsis : Bool

  `true` if `..` was used

- explicit : Bool

  `true` if `@` modifier was used

- resultIsOutParamSupport : Bool

  If the result type of an application is the `outParam` of some local instance, then special support may be needed because type class resolution interacts poorly with coercions in this kind of situation. This flag enables the special support.

  The idea is quite simple, if the result type is the `outParam` of some local instance, we simply execute `synthesizeSyntheticMVarsUsingDefault`. We added this feature to make sure examples as follows are correctly elaborated.

      class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
        getElem (xs : Cont) (i : Idx) : Elem

      export GetElem (getElem)

      instance : GetElem (Array α) Nat α where
        getElem xs i := xs.get ⟨i, sorry⟩

      opaque f : Option Bool → Bool
      opaque g : Bool → Bool

      def bad (xs : Array Bool) : Bool :=
        let x := getElem xs 0
        f x && g x

  Without the special support, Lean fails at `g x` saying `x` has type `Option Bool` but is expected to have type `Bool`. From the user's point of view this is a bug, since `let x := getElem xs 0` clearly constrains `x` to be `Bool`, but we only obtain this information after we apply the `OfNat` default instance for `0`.

  Before converging to this solution, we have tried to create a "coercion placeholder" when `resultIsOutParamSupport = true`, but it did not work well in practice. For example, it failed in the example above.

Instances For

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

Auxiliary structure for elaborating the application `f args namedArgs`.

- f : Expr
- fType : Expr
- args : List Arg

  Remaining regular arguments.

- namedArgs : List NamedArg

  remaining named arguments to be processed.

- expectedType? : Option Expr
- etaArgs : Array (Name × Expr)

  When named arguments are provided and explicit arguments occurring before them are missing, the elaborator eta-expands the declaration. For example,

      def f (x y : Nat) := x + y
      #check f (y := 5)
      -- fun x => f x 5

  `etaArgs` stores the fresh free variables for implementing the eta-expansion. Each pair records the name to use for the binding and the fvar for the argument.

  When `..` is used, eta-expansion is disabled, and missing arguments are treated as `_`.

- toSetErrorCtx : Array MVarId

  Metavariables that we need to set the error context using the application being built.

- instMVars : Array MVarId

  Metavariables for the instance implicit arguments that have already been processed.

- propagateExpected : Bool

  The following field is used to implement the `propagateExpectedType` heuristic. It is set to `true` true when `expectedType` still has to be propagated.

- resultTypeOutParam? : Option MVarId

  If the result type may be the `outParam` of some local instance. See comment at `Context.resultIsOutParamSupport`

- foundNamedArgs : Array Name

  Valid named arguments found while traversing the function's type.

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Term.ElabAppArgs.M (α : Type) :
Type
Equations

- Lean.Elab.Term.ElabAppArgs.M = ReaderT Lean.Elab.Term.ElabAppArgs.Context (StateRefT' IO.RealWorld Lean.Elab.Term.ElabAppArgs.State Lean.Elab.TermElabM)

Instances For

source
def Lean.Elab.Term.ElabAppArgs.trySynthesizeAppInstMVars :
M Unit

Try to synthesize metavariables are `instMVars` using type class resolution. The ones that cannot be synthesized yet stay in the `instMVars` list. Remark: we use this method

- before trying to apply coercions to function,
- before unifying the expected type.

Equations

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

Instances For

source
def Lean.Elab.Term.ElabAppArgs.synthesizeAppInstMVars :
M Unit

Try to synthesize metavariables are `instMVars` using type class resolution. The ones that cannot be synthesized yet are registered.

Equations

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

Instances For

source
def Lean.Elab.Term.ElabAppArgs.eraseNamedArg (binderName : Name) :
M Unit

Remove named argument with name `binderName` from `namedArgs`.

Equations

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

Instances For

source
partial def Lean.Elab.Term.ElabAppArgs.main :
M Expr

Elaborate function application arguments.

# Eliminator-like function application elaborator #

source
structure Lean.Elab.Term.ElabElimInfo :
Type

Information about an eliminator used by the elab-as-elim elaborator. This is not to be confused with `Lean.Meta.ElimInfo`, which is for `induction` and `cases`. The elab-as-elim routine is less restrictive in what counts as an eliminator, and it doesn't need to have a strict notion of what is a "target" — all it cares about are

1. that the return type of a function is of the form `m ...` where `m` is a parameter (unlike `induction` and `cases` eliminators, the arguments to `m`, known as "discriminants", can be any expressions, not just parameters), and
2. which arguments should be eagerly elaborated, to make discriminants be as elaborated as possible for the expected type generalization procedure, and which should be postponed (since they are the "minor premises").

Note that the routine isn't doing induction/cases on particular expressions. The purpose of elab-as-elim is to successfully solve the higher-order unification problem between the return type of the function and the expected type.

- elimExpr : Expr

  The eliminator.

- elimType : Expr

  The type of the eliminator.

- motivePos : Nat

  The position of the motive parameter.

- majorsPos : Array Nat

  Positions of "major" parameters (those that should be eagerly elaborated because they can contribute to the motive inference procedure). All parameters that are neither the motive nor a major parameter are "minor" parameters. The major parameters include all of the parameters that transitively appear in the motive's arguments, as well as "first-order" arguments that include such parameters, since they too can help with elaborating discriminants.

  For example, in the following theorem the argument `h : a = b` should be elaborated eagerly because it contains `b`, which occurs in `motive b`.

      theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b

  For another example, the term `isEmptyElim (α := α)` is an underapplied eliminator, and it needs argument `α` to be elaborated eagerly to create a type-correct motive.

      def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ...
      example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α)

Instances For

source
def Lean.Elab.Term.instReprElabElimInfo.repr :
ElabElimInfo → Nat → Format
Equations

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

Instances For

source
instance Lean.Elab.Term.instReprElabElimInfo :
Repr ElabElimInfo
Equations

- Lean.Elab.Term.instReprElabElimInfo = { reprPrec := Lean.Elab.Term.instReprElabElimInfo.repr }

source
def Lean.Elab.Term.instInhabitedElabElimInfo.default :
ElabElimInfo
Equations

- Lean.Elab.Term.instInhabitedElabElimInfo.default = { elimExpr := default, elimType := default, motivePos := default, majorsPos := default }

Instances For

source
instance Lean.Elab.Term.instInhabitedElabElimInfo :
Inhabited ElabElimInfo
Equations

- Lean.Elab.Term.instInhabitedElabElimInfo = { default := Lean.Elab.Term.instInhabitedElabElimInfo.default }

source
def Lean.Elab.Term.getElabElimExprInfo (elimExpr : Expr) :
MetaM ElabElimInfo
Equations

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

Instances For

source
def Lean.Elab.Term.getElabElimInfo (elimName : Name) :
MetaM ElabElimInfo
Equations

- Lean.Elab.Term.getElabElimInfo elimName = do let __do_lift ← Lean.Meta.mkConstWithFreshMVarLevels elimName Lean.Elab.Term.getElabElimExprInfo __do_lift

Instances For

source
opaque Lean.Elab.Term.elabAsElim :
TagAttribute

Instructs the elaborator that applications of this function should be elaborated like an eliminator.

An eliminator is a function that returns an application of a "motive." A motive is a parameter `p` whose type is of the form `(x₁ : _) → … → (xₙ : _) → Sort _`, i.e., a function that takes in some number of arguments (referred to as "major premises") and returns a type. The arguments `x₁` through `xₙ` of the motive can be arbitrary expressions. When elaborating an eliminator application, Lean first solves for `p` by matching `p x₁ … xₙ` against the expected type, then replacing `xₙ` through `x₁` (in that order) with variables to obtain the body of `p`. The elaborator will throw an error if this process fails (i.e., the resulting motive is not type-correct) or if the expected type cannot be determined.

Eliminator elaboration can be compared to the `induction` tactic: The expected type is used as the return value of the motive, with occurrences of the major premises replaced with the arguments. When more arguments are specified than necessary, the remaining arguments are reverted into the expected type.

The automatically-generated `rec` and `casesOn` functions of inductive types are always elaborated as eliminators. Any other functions must be tagged with this attribute in order to be elaborated in this fashion.

Examples:

    @[elab_as_elim]
    def evenOddRec {motive : Nat → Sort u}
        (even : ∀ n, motive (n * 2)) (odd : ∀ n, motive (n * 2 + 1))
        (n : Nat) : motive n := sorry

    -- simple usage
    example (a : Nat) : (a * a) % 2 = a % 2 :=
      evenOddRec _ _ a
      /-
      1. basic motive is `fun n => (a + 2) % 2 = a % 2`
      2. major premise `a` substituted: `fun n => (n + 2) % 2 = n % 2`
      3. now elaborate the other parameters as usual:
        "even" (first hole): expected type `∀ n, ((n * 2) * (n * 2)) % 2 = (n * 2) % 2`,
        "odd" (second hole): expected type `∀ n, ((n * 2 + 1) * (n * 2 + 1)) % 2 = (n * 2 + 1) % 2`
      -/

    -- complex substitution
    example (a : Nat) (f : Nat → Nat) : (f a + 1) % 2 ≠ f a :=
      evenOddRec _ _ (f a)
      /-
      Similar to before, except `f a` is substituted: `motive := fun n => (n + 1) % 2 ≠ n`.
      Now the first hole has expected type `∀ n, (n * 2 + 1) % 2 ≠ n * 2`.
      Now the second hole has expected type `∀ n, (n * 2 + 1 + 1) % 2 ≠ n * 2 + 1`.

      Note that while this might appear to work even if the `elab_as_elim` attribute is omitted from
      `evenOddRec`, the inferred motive if one does so (`fun n => (f a + 1) % 2 ≠ n`) is, in fact,
      insufficiently general: the first hole, for example, ends up with expected type
      `∀ (n : Nat), (f a + 1) % 2 ≠ n * 2`, leaving the first `f a` unsubstituted.
      -/

    -- more parameters
    example (a : Nat) (h : a % 2 = 1) : (a + 1) % 2 = 0 :=
      evenOddRec _ _ a h
      /-
      Before substitution, `a % 2 = 1` is reverted: `motive := fun n => a % 2 = 0 → (a + 1) % 2 = 0`.
      Substitution: `motive := fun n => n % 2 = 1 → (n + 1) % 2 = 0`
      Now the first hole has expected type `∀ n, n * 2 % 2 = 1 → (n * 2) % 2 = 0`.
      Now the second hole has expected type `∀ n, (n * 2 + 1) % 2 = 1 → (n * 2 + 1) % 2 = 0`.
      -/

See also `@[induction_eliminator]` and `@[cases_eliminator]` for registering default eliminators.

source
structure Lean.Elab.Term.ElabElim.Context :
Type

Context of the `elab_as_elim` elaboration procedure.

- elimInfo : ElabElimInfo
- expectedType : Expr

Instances For

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

State of the `elab_as_elim` elaboration procedure.

- f : Expr

  The resultant expression being built.

- fType : Expr

  `f : fType

- namedArgs : List NamedArg

  User-provided named arguments that still have to be processed.

- args : List Arg

  User-provided arguments that still have to be processed.

- instMVars : Array MVarId

  Instance implicit arguments collected so far.

- idx : Nat

  Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant.

- motive? : Option Expr

  Store the metavariable used to represent the motive that will be computed at `finalize`.

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Term.ElabElim.M (α : Type) :
Type
Equations

- Lean.Elab.Term.ElabElim.M = ReaderT Lean.Elab.Term.ElabElim.Context (StateRefT' IO.RealWorld Lean.Elab.Term.ElabElim.State Lean.Elab.TermElabM)

Instances For

source
def Lean.Elab.Term.ElabElim.mkMotive (discrs : Array Expr) (expectedType : Expr) :
MetaM Expr

Infer the `motive` using the expected type by `kabstract`ing the discriminants.

Equations

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

Instances For

source
def Lean.Elab.Term.ElabElim.revertArgs (args : List Arg) (f expectedType : Expr) :
TermElabM (Expr × Expr)

If the eliminator is over-applied, we "revert" the extra arguments. Returns the function with the reverted arguments applied and the new generalized expected type.

Equations

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

Instances For

source
def Lean.Elab.Term.ElabElim.finalize :
M Expr

Construct the resulting application after all discriminants have been elaborated, and we have consumed as many given arguments as possible.

Equations

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

Instances For

source
def Lean.Elab.Term.ElabElim.getNextArg? (binderName : Name) (binderInfo : BinderInfo) :
M (LOption Arg)

Return the next argument to be processed. The result is `.none` if it is an implicit argument which was not provided using a named argument. The result is `.undef` if `args` is empty and `namedArgs` does contain an entry for `binderName`.

Equations

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

Instances For

source
def Lean.Elab.Term.ElabElim.setMotive (motive : Expr) :
M Unit

Set the `motive` field in the state.

Equations

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

Instances For

source
def Lean.Elab.Term.ElabElim.saveArgInfo (arg : Expr) (binderName : Name) :
M Unit

Save information for producing error messages.

Equations

- Lean.Elab.Term.ElabElim.saveArgInfo arg binderName = if arg.isMVar = true then liftM (Lean.Elab.Term.registerMVarArgName arg.mvarId! binderName) else pure PUnit.unit

Instances For

source
def Lean.Elab.Term.ElabElim.mkImplicitArg (argExpectedType : Expr) (bi : BinderInfo) :
M Expr

Create an implicit argument using the given `BinderInfo`.

Equations

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

Instances For

source
partial def Lean.Elab.Term.ElabElim.main :
M Expr

Main loop of the `elabAsElim` procedure.

# Function application elaboration #

source
def Lean.Elab.Term.elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis : Bool) (resultIsOutParamSupport : Bool := true) :
TermElabM Expr

Elaborate a `f`-application using `namedArgs` and `args` as the arguments.

- `expectedType?` the expected type if available. It is used to propagate typing information only. This method does not ensure the result has this type.
- `explicit = true` when notation `@` is used, and implicit arguments are assumed to be provided at `namedArgs` and `args`.
- `ellipsis = true` when notation `..` is used. That is, we add `_` for missing arguments.
- `resultIsOutParamSupport` is used to control whether special support is used when processing applications of functions that return output parameter of some local instance. Example:

      GetElem.getElem : {Cont : Type u_1} → {Idx : Type u_2} → {elem : Type u_3} → {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] → (xs : cont) → (i : idx) → dom xs i → elem

  The result type `elem` is the output parameter of the local instance `self`. When this parameter is set to `true`, we execute `synthesizeSyntheticMVarsUsingDefault`. For additional details, see comment at `ElabAppArgs.resultIsOutParam`.

Equations

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

Instances For

source
inductive Lean.Elab.Term.LValResolution :
Type

Auxiliary inductive datatype that represents the resolution of an `LVal`.

- projFn (baseStructName structName fieldName : Name) : LValResolution

  When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`. This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied.

- projIdx (structName : Name) (idx : Nat) : LValResolution

  Similar to `projFn`, but for extracting field indexed by `idx`. Works for structure-like inductive types in general.

- const (baseStructName structName constName : Name) : LValResolution

  When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`, in which case these do not need to be structures. Supports generalized field notation.

- localRec (baseName : Name) (fvar : Expr) : LValResolution

  Like `const`, but with `fvar` instead of `constName`. The `baseName` is the base name of the type to search for in the parameter list.

Instances For

source
def Lean.Elab.Term.elabExplicitUnivs (lvls : Array Syntax) :
TermElabM (List Level)
Equations

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

Instances For

# Interaction between `errToSorry` and `observing`. #

- The method `elabTerm` catches exceptions, logs them, and returns a synthetic sorry (IF `ctx.errToSorry` == true).

- When we elaborate choice nodes (and overloaded identifiers), we track multiple results using the `observing x` combinator. The `observing x` executes `x` and returns a `TermElabResult`.

`observing x` does not check for synthetic sorry's, just an exception. Thus, it may think `x` worked when it didn't if a synthetic sorry was introduced. We decided that checking for synthetic sorrys at `observing` is not a good solution because it would not be clear to decide what the "main" error message for the alternative is. When the result contains a synthetic `sorry`, it is not clear which error message corresponds to the `sorry`. Moreover, while executing `x`, many error messages may have been logged. Recall that we need an error per alternative at `mergeFailures`.

Thus, we decided to set `errToSorry` to `false` whenever processing choice nodes and overloaded symbols.

Important: we rely on the property that after `errToSorry` is set to false, no elaboration function executed by `x` will reset it to `true`.

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

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

Instances For

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

- Lean.Elab.Term.elabIdent = Lean.Elab.Term.elabAtom✝

Instances For

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

- Lean.Elab.Term.elabNamedPattern = Lean.Elab.Term.elabAtom✝

Instances For

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

- Lean.Elab.Term.elabDotIdent = Lean.Elab.Term.elabAtom✝

Instances For

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

- Lean.Elab.Term.elabExplicitUniv = Lean.Elab.Term.elabAtom✝

Instances For

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

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

Instances For

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

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

Instances For

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

- Lean.Elab.Term.elabChoice = Lean.Elab.Term.elabAtom✝

Instances For

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

- Lean.Elab.Term.elabProj = Lean.Elab.Term.elabAtom✝

Instances For