Commit 2023-02-13 18:09 10b90b7a

View on Github →

chore: rename register_tag_attr, and explain relation to registerTagAttribute (#2124) Per zulip.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Tactic/LabelAttr.lean

added def Mathlib.Tactic.LabelAttr.labelled

added def Mathlib.Tactic.LabelAttr.mkLabelAttr

added def Mathlib.Tactic.LabelAttr.mkLabelExt

added def Mathlib.Tactic.LabelAttr.registerLabelAttr

Modified Mathlib/Tactic/SolveByElim.lean

Deleted Mathlib/Tactic/TagAttr.lean

deleted def Mathlib.Tactic.TagAttr.mkTagAttr

deleted def Mathlib.Tactic.TagAttr.mkTagExt

deleted def Mathlib.Tactic.TagAttr.registerTagAttr

deleted def Mathlib.Tactic.TagAttr.tagged

Modified test/solve_by_elim/basic.lean

modified theorem le_rfl