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.

Equations

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

inductive Mathlib.Tactic.BehaviorIfUnchanged : Type

Different settings of communicating about a tactic which made no progress: do nothing (keep silent), print a warning or throw an error.

• silent : BehaviorIfUnchanged

  Stay silent if this action has no effect.

• warning : BehaviorIfUnchanged

  Log a warning if this action has no effect.

• error : BehaviorIfUnchanged

  Throw an error if this action has no effect.

def Mathlib.Tactic.instBEqBehaviorIfUnchanged.beq : BehaviorIfUnchanged → BehaviorIfUnchanged → Bool

Equations

• Mathlib.Tactic.instBEqBehaviorIfUnchanged.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Mathlib.Tactic.instBEqBehaviorIfUnchanged : BEq BehaviorIfUnchanged

Equations

• Mathlib.Tactic.instBEqBehaviorIfUnchanged = { beq := Mathlib.Tactic.instBEqBehaviorIfUnchanged.beq }

@[implicit_reducible]

instance Mathlib.Tactic.instInhabitedBehaviorIfUnchanged : Inhabited BehaviorIfUnchanged

Equations

• Mathlib.Tactic.instInhabitedBehaviorIfUnchanged = { default := Mathlib.Tactic.instInhabitedBehaviorIfUnchanged.default }

def Mathlib.Tactic.instInhabitedBehaviorIfUnchanged.default : BehaviorIfUnchanged

Equations

• Mathlib.Tactic.instInhabitedBehaviorIfUnchanged.default = Mathlib.Tactic.BehaviorIfUnchanged.silent

def Mathlib.Tactic.instReprBehaviorIfUnchanged.repr : BehaviorIfUnchanged → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Mathlib.Tactic.instReprBehaviorIfUnchanged : Repr BehaviorIfUnchanged

Equations

• Mathlib.Tactic.instReprBehaviorIfUnchanged = { reprPrec := Mathlib.Tactic.instReprBehaviorIfUnchanged.repr }

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

Use the procedure m to rewrite the provided goal.

Assumes proc is not surrounded by backticks.

Equations

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

def Mathlib.Tactic.transformAtLocalDecl (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (ifUnchanged : BehaviorIfUnchanged) (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.

Assumes proc is not surrounded by backticks.

Equations

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

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) (ifUnchanged : BehaviorIfUnchanged := BehaviorIfUnchanged.error) (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).

Assumes proc is not surrounded by backticks.

Equations

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

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) (ifUnchanged : BehaviorIfUnchanged := BehaviorIfUnchanged.error) (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.

Assumes proc is not surrounded by backticks.

Equations

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