true if .. was used
ellipsis : Bool
true if @ modifier was used
explicit : 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 users point of view this is a bug, since let x := getElem xs 0 clearly constraints 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.
resultIsOutParamSupport : Bool

Instances For

source

structure Lean.Elab.Term.ElabAppArgs.State :

Type

f : Lean.Expr
fType : Lean.Expr
Remaining regular arguments.
args : List Lean.Elab.Term.Arg
remaining named arguments to be processed.
namedArgs : List Lean.Elab.Term.NamedArg
expectedType? : Option Lean.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. When .. is used, eta-expansion is disabled, and missing arguments are treated as _.
etaArgs : Array Lean.Expr
Metavariables that we need the set the error context using the application being built.
toSetErrorCtx : Array Lean.MVarId
Metavariables for the instance implicit arguments that have already been processed.
instMVars : Array Lean.MVarId
The following field is used to implement the propagateExpectedType heuristic. It is set to true true when expectedType still has to be propagated.
propagateExpected : Bool
If the result type may be the outParam of some local instance. See comment at Context.resultIsOutParamSupport
resultTypeOutParam? : Option Lean.MVarId

Auxiliary structure for elaborating the application f args namedArgs.

Instances For

source

@[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)

source

def Lean.Elab.Term.ElabAppArgs.trySynthesizeAppInstMVars :

Lean.Elab.Term.ElabAppArgs.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.

source

def Lean.Elab.Term.ElabAppArgs.synthesizeAppInstMVars :

Lean.Elab.Term.ElabAppArgs.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.

source

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

Lean.Elab.Term.ElabAppArgs.M Unit

Remove named argument with name binderName from namedArgs.

Equations

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

source

partial def Lean.Elab.Term.ElabAppArgs.main :

Lean.Elab.Term.ElabAppArgs.M Lean.Expr

Elaborate function application arguments.

source

opaque Lean.Elab.Term.elabAsElim :

Lean.TagAttribute

Eliminator-like function application elaborator #

source

structure Lean.Elab.Term.ElabElim.Context :

Type

elimInfo : Lean.Meta.ElimInfo
expectedType : Lean.Expr
Position of additonal arguments that should be elabored eagerly because they can contribute to the motive inference procedure. 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
```
extraArgsPos : Array Nat

Context of the elab_as_elim elaboration procedure.

Instances For

source

structure Lean.Elab.Term.ElabElim.State :

Type

The resultant expression being built.
f : Lean.Expr
`f : fType
fType : Lean.Expr
User-provided named arguments that still have to be processed.
namedArgs : List Lean.Elab.Term.NamedArg
User-providedarguments that still have to be processed.
args : List Lean.Elab.Term.Arg
Discriminants processed so far.
discrs : Array Lean.Expr
Instance implicit arguments collected so far.
instMVars : Array Lean.MVarId
Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant.
idx : Nat
Store the metavariable used to represent the motive that will be computed at finalize.
motive? : Option Lean.Expr

State of the elab_as_elim elaboration procedure.

Instances For

source

@[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)

source

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

Lean.MetaM Lean.Expr

Infer the motive using the expected type by kabstracting the discriminants.

Equations

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

source

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

Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)

If the eliminator is over-applied, we "revert" the extra arguments.

Equations

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

source

def Lean.Elab.Term.ElabElim.finalize :

Lean.Elab.Term.ElabElim.M Lean.Expr

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

Equations

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

source

def Lean.Elab.Term.ElabElim.getNextArg? (binderName : Lean.Name) (binderInfo : Lean.BinderInfo) :

Lean.Elab.Term.ElabElim.M (Lean.LOption Lean.Elab.Term.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.

source

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

Lean.Elab.Term.ElabElim.M Unit

Set the motive field in the state.

Equations

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

source

def Lean.Elab.Term.ElabElim.addDiscr (discr : Lean.Expr) :

Lean.Elab.Term.ElabElim.M Unit

Push the given expression into the discrs field in the state.

Equations

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

source

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

Lean.Elab.Term.ElabElim.M Unit

Save information for producing error messages.

Equations

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

source

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

Lean.Elab.Term.ElabElim.M Lean.Expr

Create an implicit argument using the given BinderInfo.

Equations

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

source

partial def Lean.Elab.Term.ElabElim.main :

Lean.Elab.Term.ElabElim.M Lean.Expr

Main loop of the elimAsElab procedure.

Function application elaboration #

source

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

Lean.Elab.TermElabM Lean.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.

source

def Lean.Elab.Term.elabAppArgs.elabAsElim? (f : Lean.Expr) (namedArgs : Array Lean.Elab.Term.NamedArg) (explicit : Bool) (ellipsis : Bool) :

Lean.Elab.TermElabM (Option Lean.Meta.ElimInfo)

Return some info if we should elaborate as an eliminator.

Equations

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

source

def Lean.Elab.Term.elabAppArgs.getElabAsElimExtraArgsPos (elimInfo : Lean.Meta.ElimInfo) :

Lean.MetaM (Array Nat)

Collect extra argument positions that must be elaborated eagerly when using elab_as_elim. The idea is that the contribute to motive inference. See comment at ElamElim.Context.extraArgsPos.

Equations

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

source

def Lean.Elab.Term.elabAppArgs.isFirstOrder (e : Lean.Expr) :

Bool

Equations

Lean.Elab.Term.elabAppArgs.isFirstOrder e = Option.isNone (Lean.Expr.find? (fun e => Lean.Expr.isApp e && !Lean.Expr.isConst (Lean.Expr.getAppFn e)) e)

source

inductive Lean.Elab.Term.LValResolution :

Type

projFn: Lean.Name → Lean.Name → Lean.Name → Lean.Elab.Term.LValResolution
projIdx: Lean.Name → Nat → Lean.Elab.Term.LValResolution
const: Lean.Name → Lean.Name → Lean.Name → Lean.Elab.Term.LValResolution
localRec: Lean.Name → Lean.Name → Lean.Expr → Lean.Elab.Term.LValResolution

Auxiliary inductive datatype that represents the resolution of an LVal.

Instances For

source

def Lean.Elab.Term.elabExplicitUnivs (lvls : Array Lean.Syntax) :

Lean.Elab.TermElabM (List Lean.Level)

Equations

Lean.Elab.Term.elabExplicitUnivs lvls = Array.foldrM (fun stx lvls => do let __do_lift ← Lean.Elab.Term.elabLevel stx pure (__do_lift :: lvls)) [] lvls (Array.size lvls)

Interaction between `errToSorry` and `observing`. #

The method elabTerm catches exceptions, log 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 :

Lean.Elab.Term.TermElab

Equations