nth_rewrite tactic

The tactic nth_rewrite and nth_rw are variants of rewrite and rw that only performs the nth possible rewrite.

ink

def Mathlib.Tactic.rewriteTarget' (stx : Lean.Syntax) (symm : Bool) (occs : optParam Lean.Occurrences Lean.Occurrences.all) (config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true }) : Lean.Elab.Tactic.TacticM Unit

Variant of rewriteTarget that allows to use Occurrences.

This def should be in Core.

Equations

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

ink

def Mathlib.Tactic.rewriteLocalDecl' (stx : Lean.Syntax) (symm : Bool) (fvarId : Lean.FVarId) (occs : optParam Lean.Occurrences Lean.Occurrences.all) (config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true }) : Lean.Elab.Tactic.TacticM Unit

Variant of rewriteLocalDecl that allows to use Occurrences.

This def should be in Core.

Equations

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

ink

def Mathlib.Tactic.nthRewriteSeq : Lean.ParserDescr

nth_rewrite is a variant of rewrite that only changes the nth occurrence of the expression to be rewritten.

Note: The occurrences are counted beginning with 1 and not 0, this is different than in mathlib3. The translation will be handled by mathport.

Equations

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

ink

def Mathlib.Tactic.evalNthRewriteSeq : Lean.Elab.Tactic.Tactic

nth_rewrite is a variant of rewrite that only changes the nth occurrence of the expression to be rewritten.

Note: The occurrences are counted beginning with 1 and not 0, this is different than in mathlib3. The translation will be handled by mathport.

Equations

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

ink

def Mathlib.Tactic.nthRwSeq : Lean.ParserDescr

nth_rw is like nth_rewrite, but also tries to close the goal by trying rfl afterwards.

Equations

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