Rewriting at specified locations

Many metaprograms have the following general structure: the input is an expression e and the output is a new expression e', together with a proof that e = e'.

This file provides convenience functions to turn such a metaprogram into a variety of tactics: using the metaprogram to modify the goal, a specified hypothesis, or (via Tactic.Location) a combination of these.

def Lean.Elab.Tactic.withNondepPropLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit) (failed : MVarId → TacticM Unit) : TacticM Unit

Runs the given atLocal and atTarget methods on each of the locations selected by the given loc.

• If loc is a list of locations, runs at each specified hypothesis (and finally the goal if ⊢ is included), and fails if any of the tactic applications fail.
• If loc is *, runs at the nondependent Prop hypotheses (those produced by Lean.MVarId.getNondepPropHyps) and then at the target.

This is a variant of Lean.Elab.Tactic.withLocation.

def Mathlib.Tactic.transformAtTarget (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (failIfUnchanged : Bool) (goal : Lean.MVarId) : ReaderT Lean.Meta.Simp.Context Lean.MetaM (Option Lean.MVarId)

Use the procedure m to rewrite the provided goal.

def Mathlib.Tactic.transformAtLocalDecl (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (failIfUnchanged mayCloseGoal : Bool) (fvarId : Lean.FVarId) (goal : Lean.MVarId) : ReaderT Lean.Meta.Simp.Context Lean.MetaM (Option Lean.MVarId)

Use the procedure m to rewrite hypothesis fvarId.

The simpTheorems of the simp-context carried with m will be modified to remove fvarId; this ensures that if the procedure m involves rewriting by this SimpTheoremsArray, then, e.g., h : x = y is not transformed (by rewriting h) to True.

def Mathlib.Tactic.transformAtLocation (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (loc : Lean.Elab.Tactic.Location) (failIfUnchanged : Bool := true) (mayCloseGoalFromHyp : Bool := false) (ctx : Lean.Meta.Simp.Context := default) : Lean.Elab.Tactic.TacticM Unit

Use the procedure m to transform at specified locations (hypotheses and/or goal).

def Mathlib.Tactic.transformAtNondepPropLocation (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (loc : Lean.Elab.Tactic.Location) (failIfUnchanged : Bool := true) (mayCloseGoalFromHyp : Bool := false) (ctx : Lean.Meta.Simp.Context := default) : Lean.Elab.Tactic.TacticM Unit

Use the procedure m to transform at specified locations (hypotheses and/or goal).

In the wildcard case (*), filter out all dependent and/or non-Prop hypotheses.