# Miscellaneous helper functions for tactics. #

[TODO] Ideally we would find good homes for everything in this file, eventually removing it.

source
def Mathlib.Tactic.modifyMetavarDecl {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (f : Lean.MetavarDecl → Lean.MetavarDecl) :
m Unit

`modifyMetavarDecl mvarId f` updates the `MetavarDecl` for `mvarId` with `f`. Conditions on `f`:

- The target of `f mdecl` is defeq to the target of `mdecl`.
- The local context of `f mdecl` must contain the same fvars as the local context of `mdecl`. For each fvar in the local context of `f mdecl`, the type (and value, if any) of the fvar must be defeq to the corresponding fvar in the local context of `mdecl`.

If `mvarId` does not refer to a declared metavariable, nothing happens.

Equations

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

Instances For

source
def Mathlib.Tactic.modifyTarget {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.Expr) :
m Unit

`modifyTarget mvarId f` updates the target of the metavariable `mvarId` with `f`. For any `e`, `f e` must be defeq to `e`. If `mvarId` does not refer to a declared metavariable, nothing happens.

Equations

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

Instances For

source
def Mathlib.Tactic.modifyLocalContext {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (f : Lean.LocalContext → Lean.LocalContext) :
m Unit

`modifyLocalContext mvarId f` updates the local context of the metavariable `mvarId` with `f`. The new local context must contain the same fvars as the old local context and the types (and values, if any) of the fvars in the new local context must be defeq to their equivalents in the old local context.

If `mvarId` does not refer to a declared metavariable, nothing happens.

Equations

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

Instances For

source
def Mathlib.Tactic.modifyLocalDecl {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (f : Lean.LocalDecl → Lean.LocalDecl) :
m Unit

`modifyLocalDecl mvarId fvarId f` updates the local decl `fvarId` in the local context of `mvarId` with `f`. `f` must leave the `fvarId` and `index` of the `LocalDecl` unchanged. The type of the new `LocalDecl` must be defeq to the type of the old `LocalDecl` (and the same applies to the value of the `LocalDecl`, if any).

If `mvarId` does not refer to a declared metavariable or if `fvarId` does not exist in the local context of `mvarId`, nothing happens.

Equations

- Mathlib.Tactic.modifyLocalDecl mvarId fvarId f = Mathlib.Tactic.modifyLocalContext mvarId fun (lctx : Lean.LocalContext) => lctx.modifyLocalDecl fvarId f

Instances For