# Documentation

Lean.MetavarContext

The metavariable context stores metavariable declarations and their assignments. It is used in the elaborator, tactic framework, unifier (aka isDefEq), and type class resolution (TC). First, we list all the requirements imposed by these modules.

• We may invoke TC while executing isDefEq. We need this feature to be able to solve unification problems such as:
f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m


where (?a : Type) (?s : Ring ?a) (?x ?y : ?a) During isDefEq (i.e., unification), it will need to solve the constrain

ringAdd ?s =?= intAdd


We say ringAdd ?s is stuck because it cannot be reduced until we synthesize the term ?s : Ring ?a using TC. This can be done since we have assigned ?a := Int when solving ?a =?= Int.

• TC uses isDefEq, and isDefEq may create TC problems as shown above. Thus, we may have nested TC problems.

• isDefEq extends the local context when going inside binders. Thus, the local context for nested TC may be an extension of the local context for outer TC.

• TC should not assign metavariables created by the elaborator, simp, tactic framework, and outer TC problems. Reason: TC commits to the first solution it finds. Consider the TC problem Coe Nat ?x, where ?x is a metavariable created by the caller. There are many solutions to this problem (e.g., ?x := Int, ?x := Real, ...), and it doesn’t make sense to commit to the first one since TC does not know the constraints the caller may impose on ?x after the TC problem is solved. Remark: we claim it is not feasible to make the whole system backtrackable, and allow the caller to backtrack back to TC and ask it for another solution if the first one found did not work. We claim it would be too inefficient.

• TC metavariables should not leak outside of TC. Reason: we want to get rid of them after we synthesize the instance.

• simp invokes isDefEq for matching the left-hand-side of equations to terms in our goal. Thus, it may invoke TC indirectly.

• In Lean3, we didn’t have to create a fresh pattern for trying to match the left-hand-side of equations when executing simp. We had a mechanism called "tmp" metavariables. It avoided this overhead, but it created many problems since simp may indirectly call TC which may recursively call TC. Moreover, we may want to allow TC to invoke tactics in the future. Thus, when simp invokes isDefEq, it may indirectly invoke a tactic and simp itself. The Lean3 approach assumed that metavariables were short-lived, this is not true in Lean4, and to some extent was also not true in Lean3 since simp, in principle, could trigger an arbitrary number of nested TC problems.

• Here are some possible call stack traces we could have in Lean3 (and Lean4).

Elaborator (-> TC -> isDefEq)+
Elaborator -> isDefEq (-> TC -> isDefEq)*
Elaborator -> simp -> isDefEq (-> TC -> isDefEq)*


In Lean4, TC may also invoke tactics in the future.

• In Lean3 and Lean4, TC metavariables are not really short-lived. We solve an arbitrary number of unification problems, and we may have nested TC invocations.

• TC metavariables do not share the same local context even in the same invocation. In the C++ and Lean implementations we use a trick to ensure they do: https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L3583-L3594

• Metavariables may be natural, synthetic or syntheticOpaque. a) Natural metavariables may be assigned by unification (i.e., isDefEq).

b) Synthetic metavariables may still be assigned by unification, but whenever possible isDefEq will avoid the assignment. For example, if we have the unification constraint ?m =?= ?n, where ?m is synthetic, but ?n is not, isDefEq solves it by using the assignment ?n := ?m. We use synthetic metavariables for type class resolution. Any module that creates synthetic metavariables, must also check whether they have been assigned by isDefEq, and then still synthesize them, and check whether the synthesized result is compatible with the one assigned by isDefEq.

c) SyntheticOpaque metavariables are never assigned by isDefEq. That is, the constraint ?n =?= Nat.succ Nat.zero always fail if ?n is a syntheticOpaque metavariable. This kind of metavariable is created by tactics such as intro. Reason: in the tactic framework, subgoals as represented as metavariables, and a subgoal ?n is considered as solved whenever the metavariable is assigned.

This distinction was not precise in Lean3 and produced counterintuitive behavior. For example, the following hack was added in Lean3 to work around one of these issues: https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L2751

• When creating lambda/forall expressions, we need to convert/abstract free variables and convert them to bound variables. Now, suppose we are trying to create a lambda/forall expression by abstracting free variable xs and a term t[?m] which contains a metavariable ?m, and the local context of ?m contains xs. The term

fun xs => t[?m]


will be ill-formed if we later assign a term s to ?m, and s contains free variables in xs. We address this issue by changing the free variable abstraction procedure. We consider two cases: ?m is natural or synthetic, or ?m is syntheticOpaque. Assume the type of ?m is A[xs]. Then, in both cases we create an auxiliary metavariable ?n with type forall xs => A[xs], and local context := local context of ?m - xs. In both cases, we produce the term fun xs => t[?n xs]

1- If ?m is natural or synthetic, then we assign ?m := ?n xs, and we produce the term fun xs => t[?n xs]

2- If ?m is syntheticOpaque, then we mark ?n as a syntheticOpaque variable. However, ?n is managed by the metavariable context itself. We say we have a "delayed assignment" ?n xs := ?m. That is, after a term s is assigned to ?m, and s does not contain metavariables, we replace any occurrence ?n ts with s[xs := ts].

Gruesome details:

• When we create the type forall xs => A for ?n, we may encounter the same issue if A contains metavariables. So, the process above is recursive. We claim it terminates because we keep creating new metavariables with smaller local contexts.

• Suppose, we have t[?m] and we want to create a let-expression by abstracting a let-decl free variable x, and the local context of ?m contains x. Similarly to the previous case

let x : T := v; t[?m]


will be ill-formed if we later assign a term s to ?m, and s contains free variable x. Again, assume the type of ?m is A[x].

1- If ?m is natural or synthetic, then we create ?n : (let x : T := v; A[x]) with
and local context := local context of ?m - x, we assign ?m := ?n,
and produce the term let x : T := v; t[?n]. That is, we are just making
sure ?n must never be assigned to a term containing x.

2- If ?m is syntheticOpaque, we create a fresh syntheticOpaque ?n
with type ?n : T -> (let x : T := v; A[x]) and local context := local context of ?m - x,
create the delayed assignment ?n #[x] := ?m, and produce the term let x : T := v; t[?n x].
Now suppose we assign s to ?m. We do not assign the term fun (x : T) => s to ?n, since
fun (x : T) => s may not even be type correct. Instead, we just replace applications ?n r
with s[x/r]. The term r may not necessarily be a bound variable. For example, a tactic
may have reduced let x : T := v; t[?n x] into t[?n v].
We are essentially using the pair "delayed assignment + application" to implement a delayed
substitution.

• We use TC for implementing coercions. Both Joe Hendrix and Reid Barton reported a nasty limitation. In Lean3, TC will not be used if there are metavariables in the TC problem. For example, the elaborator will not try to synthesize Coe Nat ?x. This is good, but this constraint is too strict for problems such as Coe (Vector Bool ?n) (BV ?n). The coercion exists independently of ?n. Thus, during TC, we want isDefEq to throw an exception instead of return false whenever it tries to assign a metavariable owned by its caller. The idea is to sign to the caller that it cannot solve the TC problem at this point, and more information is needed. That is, the caller must make progress an assign its metavariables before trying to invoke TC again.

In Lean4, we are using a simpler design for the MetavarContext.

• No distinction between temporary and regular metavariables.

• Metavariables have a depth Nat field.

• MetavarContext also has a depth field.

• We bump the MetavarContext depth when we create a nested problem. Example: Elaborator (depth = 0) -> Simplifier matcher (depth = 1) -> TC (level = 2) -> TC (level = 3) -> ...

• When MetavarContext is at depth N, isDefEq does not assign variables from depth < N.

• Metavariables from depth N+1 must be fully assigned before we return to level N.

• New design even allows us to invoke tactics from TC.

• Main concern We don't have tmp metavariables anymore in Lean4. Thus, before trying to match the left-hand-side of an equation in simp. We first must bump the level of the MetavarContext, create fresh metavariables, then create a new pattern by replacing the free variable on the left-hand-side with these metavariables. We are hoping to minimize this overhead by

• Using better indexing data structures in simp. They should reduce the number of time simp must invoke isDefEq.

• Implementing isDefEqApprox which ignores metavariables and returns only false or undef. It is a quick filter that allows us to fail quickly and avoid the creation of new fresh metavariables, and a new pattern.

• Adding built-in support for arithmetic, Logical connectives, etc. Thus, we avoid a bunch of lemmas in the simp set.

• Adding support for AC-rewriting. In Lean3, users use AC lemmas as rewriting rules for "sorting" terms. This is inefficient, requires a quadratic number of rewrite steps, and does not preserve the structure of the goal.

The temporary metavariables were also used in the "app builder" module used in Lean3. The app builder uses isDefEq. So, it could, in principle, invoke an arbitrary number of nested TC problems. However, in Lean3, all app builder uses are controlled. That is, it is mainly used to synthesize implicit arguments using very simple unification and/or non-nested TC. So, if the "app builder" becomes a bottleneck without tmp metavars, we may solve the issue by implementing isDefEqCheap that never invokes TC and uses tmp metavars.

LocalInstance represents a local typeclass instance registered by and for the elaborator. It stores the name of the typeclass in className, and the concrete typeclass instance in fvar. Note that the kernel does not care about this information, since typeclasses are entirely eliminated during elaboration.

Instances For
Equations
@[inline]
Equations
Equations
Equations

Remove local instance with the given fvarId. Do nothing if localInsts does not contain any free variable with id fvarId.

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

A kind for the metavariable that determines its unification behaviour. For more information see the large comment at the beginning of this file.

Instances For
Equations
• = match x with | Lean.MetavarKind.syntheticOpaque => true | x => false
Equations
• = match x with | Lean.MetavarKind.natural => true | x => false
• A user-friendly name for the metavariable. If anonymous then there is no such name.

• The local context containing the free variables that the mvar is permitted to depend upon.

• The type of the metavarible, in the given lctx.

type : Lean.Expr
• The nesting depth of this metavariable. We do not want unification subproblems to influence the results of parent problems. The depth keeps track of this information and ensures that unification subproblems cannot leak information out, by unifying based on depth.

depth : Nat
• localInstances : Lean.LocalInstances
• See comment at CheckAssignment Meta/ExprDefEq.lean

numScopeArgs : Nat
• We use this field to track how old a metavariable is. It is set using a counter at MetavarContext

index : Nat

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

A delayed assignment for a metavariable ?m. It represents an assignment of the form ?m := (fun fvars => (mkMVar mvarIdPending)). mvarIdPending is a syntheticOpaque metavariable that has not been synthesized yet. The delayed assignment becomes a real one as soon as mvarIdPending has been fully synthesized. fvars are variables in the mvarIdPending local context.

See the comment below assignDelayedMVar  for the rationale of delayed assignments.

Recall that we use a locally nameless approach when dealing with binders. Suppose we are trying to synthesize ?n in the expression e, in the context of (fun x => e). The metavariable ?n might depend on the bound variable x. However, since we are locally nameless, the bound variable x is in fact represented by some free variable fvar_x. Thus, when we exit the scope, we must rebind the value of fvar_x in ?n to the de-bruijn index of the bound variable x.

Instances For
• Depth is used to control whether an mvar can be assigned in unification.

depth : Nat
• At what depth level mvars can be assigned.

levelAssignDepth : Nat
• Counter for setting the field index at MetavarDecl

mvarCounter : Nat
• lDepth :
• Metavariable declarations.

• Index mapping user-friendly names to ids.

• Assignment table for universe level metavariables.

lAssignment :
• Assignment table for expression metavariables.

eAssignment :
• Assignment table for delayed abstraction metavariables. For more information about delayed abstraction, see the docstring for DelayedMetavarAssignment.

The metavariable context is a set of metavariable declarations and their assignments.

For more information on specifics see the comment in the file that MetavarContext is defined in.

Instances For
class Lean.MonadMCtx (m : ) :
• getMCtx :
• modifyMCtx :

A monad with a stateful metavariable context, defining getMCtx and modifyMCtx.

Instances
@[always_inline]
instance Lean.instMonadMCtx (m : ) (n : ) [inst : ] [inst : ] :
Equations
• = { getMCtx := liftM Lean.getMCtx, modifyMCtx := fun f => }
@[inline]
abbrev Lean.setMCtx {m : } [inst : ] (mctx : Lean.MetavarContext) :
Equations
@[inline]
abbrev Lean.getLevelMVarAssignment? {m : } [inst : ] [inst : ] (mvarId : Lean.LMVarId) :
m ()
Equations
def Lean.getExprMVarAssignment? {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :
m ()
Equations
def Lean.getDelayedMVarAssignment? {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :
Equations
partial def Lean.getDelayedMVarRoot {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :

Given a sequence of delayed assignments

mvarId₁ := mvarId₂ ...;
...
mvarIdₙ := mvarId_root ...  -- where mvarId_root is not delayed assigned


in mctx, getDelayedRoot mctx mvarId₁ return mvarId_root. If mvarId₁ is not delayed assigned then return mvarId₁

def Lean.isLevelMVarAssigned {m : } [inst : ] [inst : ] (mvarId : Lean.LMVarId) :
Equations
def Lean.MVarId.isAssigned {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :

Return true if the give metavariable is already assigned.

Equations
def Lean.isExprMVarAssigned {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :
Equations
def Lean.MVarId.isDelayedAssigned {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :
Equations
def Lean.isMVarDelayedAssigned {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :
Equations
def Lean.isLevelMVarAssignable {m : } [inst : ] [inst : ] (mvarId : Lean.LMVarId) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.MVarId.isAssignable {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :
Equations
def Lean.isExprMVarAssignable {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :
Equations
def Lean.hasAssignedLevelMVar {m : } [inst : ] [inst : ] :

Return true iff the given level contains an assigned metavariable.

Equations
def Lean.hasAssignedMVar {m : } [inst : ] [inst : ] :

Return true iff expression contains assigned (level/expr) metavariables or delayed assigned mvars

Equations
def Lean.hasAssignableLevelMVar {m : } [inst : ] [inst : ] :

Return true iff the given level contains a metavariable that can be assigned.

Equations
• One or more equations did not get rendered due to their size.
def Lean.hasAssignableMVar {m : } [inst : ] [inst : ] :

Return true iff expression contains a metavariable that can be assigned.

Equations
def Lean.assignLevelMVar {m : } [inst : ] (mvarId : Lean.LMVarId) (val : Lean.Level) :

Add mvarId := u to the universe metavariable assignment. This method does not check whether mvarId is already assigned, nor it checks whether a cycle is being introduced. This is a low-level API, and it is safer to use isLevelDefEq (mkLevelMVar mvarId) u.

Equations
• One or more equations did not get rendered due to their size.
def Lean.MVarId.assign {m : } [inst : ] (mvarId : Lean.MVarId) (val : Lean.Expr) :

Add mvarId := x to the metavariable assignment. This method does not check whether mvarId is already assigned, nor it checks whether a cycle is being introduced, or whether the expression has the right type. This is a low-level API, and it is safer to use isDefEq (mkMVar mvarId) x.

Equations
• One or more equations did not get rendered due to their size.
def Lean.assignExprMVar {m : } [inst : ] (mvarId : Lean.MVarId) (val : Lean.Expr) :
Equations
def Lean.assignDelayedMVar {m : } [inst : ] (mvarId : Lean.MVarId) (fvars : ) (mvarIdPending : Lean.MVarId) :
Equations
• One or more equations did not get rendered due to their size.

Notes on artificial eta-expanded terms due to metavariables. We try avoid synthetic terms such as ((fun x y => t) a b) in the output produced by the elaborator. This kind of term may be generated when instantiating metavariable assignments. This module tries to avoid their generation because they often introduce unnecessary dependencies and may affect automation.

When elaborating terms, we use metavariables to represent "holes". Each hole has a context which includes all free variables that may be used to "fill" the hole. Suppose, we create a metavariable (hole) ?m : Nat in a context containing (x : Nat) (y : Nat) (b : Bool), then we can assign terms such as x + y to ?m since x and y are in the context used to create ?m. Now, suppose we have the term ?m + 1 and we want to create the lambda expression fun x => ?m + 1. This term is not correct since we may assign to ?m a term containing x. We address this issue by create a synthetic metavariable ?n : Nat → Nat and adding the delayed assignment ?n #[x] := ?m, and the term fun x => ?n x + 1. When we later assign a term t[x] to ?m, fun x => t[x] is assigned to ?n, and if we substitute it at fun x => ?n x + 1, we produce fun x => ((fun x => t[x]) x) + 1. To avoid this term eta-expanded term, we apply beta-reduction when instantiating metavariable assignments in this module. This operation is performed at instantiateExprMVars, elimMVarDeps, and levelMVarToParam.

partial def Lean.instantiateLevelMVars {m : } [inst : ] [inst : ] :
partial def Lean.instantiateExprMVars {m : } {ω : Type} [inst : ] [inst : ] [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] (e : Lean.Expr) :

instantiateExprMVars main function

Equations
• Lean.instMonadMCtxStateRefT'MetavarContextST = { getMCtx := get, modifyMCtx := modify }
Equations
def Lean.instantiateMVars {m : } [inst : ] [inst : ] (e : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.instantiateLCtxMVars {m : } [inst : ] [inst : ] (lctx : Lean.LocalContext) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.instantiateMVarDeclMVars {m : } [inst : ] [inst : ] (mvarId : Lean.MVarId) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.instantiateLocalDeclMVars {m : } [inst : ] [inst : ] (localDecl : Lean.LocalDecl) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
@[inline]
def Lean.DependsOn.main (pf : ) (pm : ) (e : Lean.Expr) :
Equations
@[inline]
def Lean.findExprDependsOn {m : } [inst : ] [inst : ] (e : Lean.Expr) (pf : optParam () fun x => false) (pm : optParam () fun x => false) :

Return true iff e depends on a free variable x s.t. pf x is true, or an unassigned metavariable ?m s.t. pm ?m is true. For each metavariable ?m (that does not satisfy pm occurring in x 1- If ?m := t, then we visit t looking for x 2- If ?m is unassigned, then we consider the worst case and check whether x is in the local context of ?m. This case is a "may dependency". That is, we may assign a term t to ?m s.t. t contains x.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.findLocalDeclDependsOn {m : } [inst : ] [inst : ] (localDecl : Lean.LocalDecl) (pf : optParam () fun x => false) (pm : optParam () fun x => false) :

Similar to findExprDependsOn, but checks the expressions in the given local declaration depends on a free variable x s.t. pf x is true or an unassigned metavariable ?m s.t. pm ?m is true.

Equations
• One or more equations did not get rendered due to their size.
def Lean.exprDependsOn {m : } [inst : ] [inst : ] (e : Lean.Expr) (fvarId : Lean.FVarId) :
Equations
def Lean.dependsOn {m : } [inst : ] [inst : ] (e : Lean.Expr) (fvarId : Lean.FVarId) :

Return true iff e depends on the free variable fvarId

Equations
def Lean.localDeclDependsOn {m : } [inst : ] [inst : ] (localDecl : Lean.LocalDecl) (fvarId : Lean.FVarId) :

Return true iff localDecl depends on the free variable fvarId

Equations
def Lean.exprDependsOn' {m : } [inst : ] [inst : ] (e : Lean.Expr) (x : Lean.Expr) :

Similar to exprDependsOn, but x can be a free variable or an unassigned metavariable.

Equations
• One or more equations did not get rendered due to their size.
def Lean.localDeclDependsOn' {m : } [inst : ] [inst : ] (localDecl : Lean.LocalDecl) (x : Lean.Expr) :

Similar to localDeclDependsOn, but x can be a free variable or an unassigned metavariable.

Equations
• One or more equations did not get rendered due to their size.
def Lean.dependsOnPred {m : } [inst : ] [inst : ] (e : Lean.Expr) (pf : optParam () fun x => false) (pm : optParam () fun x => false) :

Return true iff e depends on a free variable x s.t. pf x, or an unassigned metavariable ?m s.t. pm ?m is true.

Equations
def Lean.localDeclDependsOnPred {m : } [inst : ] [inst : ] (localDecl : Lean.LocalDecl) (pf : optParam () fun x => false) (pm : optParam () fun x => false) :

Return true iff the local declaration localDecl depends on a free variable x s.t. pf x, an unassigned metavariable ?m s.t. pm ?m is true.

Equations
Equations
• One or more equations did not get rendered due to their size.
@[export lean_mk_metavar_ctx]
Equations
• One or more equations did not get rendered due to their size.
def Lean.MetavarContext.addExprMVarDecl (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (userName : Lean.Name) (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances) (type : Lean.Expr) (numScopeArgs : ) :

Low level API for adding/declaring metavariable declarations. It is used to implement actions in the monads MetaM, ElabM and TacticM. It should not be used directly since the argument (mvarId : MVarId) is assumed to be "unique".

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

Low level API for adding/declaring universe level metavariable declarations. It is used to implement actions in the monads MetaM, ElabM and TacticM. It should not be used directly since the argument (mvarId : MVarId) is assumed to be "unique".

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

Set the metavariable user facing name.

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

Low-level version of setMVarUserName. It does not update the table userNames. Thus, findUserName? cannot see the modification. It is meant for mkForallFVars' where we temporarily set the user facing name of metavariables to get more meaningful binder names.

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

Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• Lean.MetavarContext.instMonadMCtxStateRefT'MetavarContextST = { getMCtx := get, modifyMCtx := modify }
• revertFailure:
Instances For
Equations
• One or more equations did not get rendered due to their size.

MkBinding and elimMVarDepsAux are mutually recursive, but cache is only used at elimMVarDepsAux. We use a single state object for convenience.

We have a NameGenerator because we need to generate fresh auxiliary metavariables.

Instances For
• mainModule : Lean.Name
• preserveOrder : Bool
• When creating binders for abstracted metavariables, we use the following BinderInfo.

binderInfoForMVars : Lean.BinderInfo
• Set of unassigned metavariables being abstracted.

mvarIdsToAbstract : Lean.MVarIdSet
Instances For
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.

Given toRevert an array of free variables s.t. lctx contains their declarations, return a new array of free variables that contains toRevert and all variables in lctx that may depend on toRevert.

Remark: the result is sorted by LocalDecl indices.

Remark: We used to throw an Exception.revertFailure exception when an auxiliary declaration had to be reversed. Recall that auxiliary declarations are created when compiling (mutually) recursive definitions. The revertFailure due to auxiliary declaration dependency was originally introduced in Lean3 to address issue https://github.com/leanprover/lean/issues/1258. In Lean4, this solution is not satisfactory because all definitions/theorems are potentially recursive. So, even a simple (incomplete) definition such as

variables {α : Type} in
def f (a : α) : List α :=
_


would trigger the Exception.revertFailure exception. In the definition above, the elaborator creates the auxiliary definition f : {α : Type} → List α. The _ is elaborated as a new fresh variable ?m that contains α : Type, a : α, and f : α → List α in its context, When we try to create the lambda fun {α : Type} (a : α) => ?m, we first need to create an auxiliary ?n which does not contain α and a in its context. That is, we create the metavariable ?n : {α : Type} → (a : α) → (f : α → List α) → List α, add the delayed assignment ?n #[α, a, f] := ?m, and create the lambda fun {α : Type} (a : α) => ?n α a f. See elimMVarDeps for more information. If we kept using the Lean3 approach, we would get the Exception.revertFailure exception because we are reverting the auxiliary definition f.

Note that https://github.com/leanprover/lean/issues/1258 is not an issue in Lean4 because we have changed how we compile recursive definitions.

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

Create a new LocalContext by removing the free variables in toRevert from lctx. We use this function when we create auxiliary metavariables at elimMVarDepsAux.

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

Revert the variables xs from the local context of mvarId, returning an expression representing the (new) reverted metavariable and the list of variables that were actually reverted (this list will include any forward dependencies).

See details in the comment at the top of the file.

Equations
@[inline]

Similar to Expr.abstractRange, but handles metavariables correctly. It uses elimMVarDeps to ensure e and the type of the free variables xs do not contain a metavariable ?m s.t. local context of ?m contains a free variable in xs.

Equations
@[specialize #[]]
def Lean.MetavarContext.MkBinding.mkBinding (isLambda : Bool) (lctx : Lean.LocalContext) (xs : ) (e : Lean.Expr) (usedOnly : Bool) (usedLetOnly : Bool) :

Similar to LocalContext.mkBinding, but handles metavariables correctly. If usedOnly == true then forall and lambda expressions are created only for used variables. If usedLetOnly == true then let expressions are created only for used (let-) variables.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
def Lean.MetavarContext.elimMVarDeps (xs : ) (e : Lean.Expr) (preserveOrder : Bool) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.MetavarContext.revert (xs : ) (mvarId : Lean.MVarId) (preserveOrder : Bool) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.MetavarContext.mkBinding (isLambda : Bool) (xs : ) (e : Lean.Expr) (usedOnly : ) (usedLetOnly : ) (binderInfoForMVars : ) :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.MetavarContext.mkLambda (xs : ) (e : Lean.Expr) (usedOnly : ) (usedLetOnly : ) (binderInfoForMVars : ) :
Equations
@[inline]
def Lean.MetavarContext.mkForall (xs : ) (e : Lean.Expr) (usedOnly : ) (usedLetOnly : ) (binderInfoForMVars : ) :
Equations
@[inline]
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.MetavarContext.collectForwardDeps (toRevert : ) (preserveOrder : Bool) :
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.MetavarContext.isWellFormed {m : } [inst : ] [inst : ] (lctx : Lean.LocalContext) :

isWellFormed lctx e returns true iff

• All locals in e are declared in lctx
• All metavariables ?m in e have a local context which is a subprefix of lctx or are assigned, and the assignment is well-formed.
• paramNamePrefix : Lean.Name