Documentation

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

Set the metavariable user facing name.

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.

Return true iff the given level contains an assigned metavariable.

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

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

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

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.

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.

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

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

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 free 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 an 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 do 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 α a f, 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.

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

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.

elimMVarDeps is defined later in this file.

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