Miscellaneous helper functions for tactics.

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

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.

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.

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.

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) => Lean.LocalContext.modifyLocalDecl lctx fvarId f