source
def Lean.MVarId.replaceTargetEq (mvarId : MVarId) (targetNew eqProof : Expr) :
MetaM MVarId

Convert the given goal `Ctx |- target` into `Ctx |- targetNew` using an equality proof `eqProof : target = targetNew`. It assumes `eqProof` has type `target = targetNew`

Equations

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

Instances For

source
def Lean.MVarId.replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) :
MetaM MVarId

Converts the given goal `Ctx |- target` into `Ctx |- targetNew`. It assumes the goals are definitionally equal. We use the proof term

    @id target mvarNew

to create a checkpoint.

If `targetNew` is equal to `target`, then returns `mvarId` unchanged. Uses `Expr.equal` for the comparison so that it is possible to update binder names, etc., which are user-visible.

Equations

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

Instances For

source
@[inline]
def Lean.MVarId.replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew eqProof : Expr) :
MetaM Meta.AssertAfterResult

Replace type of the local declaration with id `fvarId` with one with the same user-facing name, but with type `typeNew`. This method assumes `eqProof` is a proof that the type of `fvarId` is equal to `typeNew`. This tactic actually adds a new declaration and (tries to) clear the old one. If the old one cannot be cleared, then at least its user-facing name becomes inaccessible.

The new local declaration is inserted at the soonest point after `fvarId` at which it is well-formed. That is, if `typeNew` involves declarations which occur later than `fvarId` in the local context, the new local declaration will be inserted immediately after the latest-occurring one. Otherwise, it will be inserted immediately after `fvarId`.

Note: `replaceLocalDecl` should not be used when unassigned pending mvars might be present in `typeNew`, as these may later be synthesized to fvars which occur after `fvarId` (by e.g. `Term.withSynthesize` or `Term.synthesizeSyntheticMVars`) .

Equations

- mvarId.replaceLocalDecl fvarId typeNew eqProof = Lean.Meta.replaceLocalDeclCore✝ mvarId fvarId typeNew eqProof

Instances For

source
def Lean.MVarId.replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) :
MetaM MVarId

Replaces the type of `fvarId` at `mvarId` with `typeNew`. Remark: this method assumes that `typeNew` is definitionally equal to the current type of `fvarId`.

If `typeNew` is equal to current type of `fvarId`, then returns `mvarId` unchanged. Uses `Expr.equal` for the comparison so that it is possible to update binder names, etc., which are user-visible.

Equations

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

Instances For

source
def Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq : Bool := true) :
MetaM MVarId

Replace the target type of `mvarId` with `typeNew`. If `checkDefEq = false`, this method assumes that `typeNew` is definitionally equal to the current target type. If `checkDefEq = true`, throw an error if `typeNew` is not definitionally equal to the current target type.

Equations

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

Instances For

source
def Lean.MVarId.withReverted {α : Type} (mvarId : MVarId) (fvarIds : Array FVarId) (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId)) (clearAuxDeclsInsteadOfRevert : Bool := false) :
MetaM (α × MVarId)

Executes the revert/intro pattern, running the continuation `k` after temporarily reverting the given local variables from the local context of the metavariable `mvarId`, and then re-introducing the local variables specified by `k`.

- `mvarId` is the goal metavariable to operate on.
- `fvarIds` is an array of `fvarIds` to revert in the order specified. An error is thrown if they cannot be reverted in order.
- `clearAuxDeclsInsteadOfRevert` is configuration passed to `Lean.MVarId.revert`.
- `k` is the continuation run once the local variables have been reverted. It is provided `mvarId` after the requested variables have been reverted along with the array of reverted variables. This array always contains `fvarIds`, but it may contain additional variables that were reverted due to dependencies. The continuation returns a value, a new goal, and an aliasing array.

Once `k` has completed, one variable is introduced per entry in the aliasing array.

- If the entry is `none`, the variable is just introduced.
- If the entry is `some fv` (where `fv` is a variable from `fvarIds`), the variable is introduced and then recorded as an alias of `fv` in the info tree. This for example causes the unused variable linter as seeing `fv` and this newly introduced variable as being "the same".

For example, if `k` leaves all the reverted variables in the same order, having it return `fvars.map .some` as the aliasing array causes those variables to be re-introduced and aliased to the original local variables.

Returns the value returned by `k` along with the resulting goal after variable introduction.

See `Lean.MVarId.changeLocalDecl` for an example. The motivation is that to work on a local variable, you need to move it into the goal, alter the goal, and then bring it back into the local context, all while keeping track of any other local variables that depend on this one.

Equations

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

Instances For

source
def Lean.MVarId.withRevertedFrom {α : Type} (mvarId : MVarId) (fvarId : FVarId) (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId)) :
MetaM (α × MVarId)

Like `Lean.MVarId.withReverted`, but reverts all local variables starting from `fvarId`.

Equations

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

Instances For

source
def Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq : Bool := true) :
MetaM MVarId

Replaces the type of the free variable `fvarId` with `typeNew`.

If `checkDefEq` is `true` then an error is thrown if `typeNew` is not definitionally equal to the type of `fvarId`. Otherwise this function assumes `typeNew` and the type of `fvarId` are definitionally equal.

Equations

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

Instances For

source
def Lean.MVarId.modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr) :
MetaM MVarId

Modify `mvarId` target type using `f`.

Equations

- mvarId.modifyTarget f = mvarId.withContext do mvarId.checkNotAssigned `modifyTarget let __do_lift ← mvarId.getType let __do_lift ← f __do_lift mvarId.change __do_lift false

Instances For

source
def Lean.MVarId.modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM Expr) :
MetaM MVarId

Modify `mvarId` target type left-hand-side using `f`. Throw an error if target type is not an equality.

Equations

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

Instances For

source
def Lean.MVarId.clearValue (mvarId : MVarId) (fvarId : FVarId) :
MetaM MVarId

Clears the value of the local definition `fvarId`. Ensures that the resulting goal state is still type correct. Throws an error if it is a local hypothesis without a value.

Preserves the order of the local context.

Equations

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

Instances For