Def Mathlib.Tactic.LabelAttr.mkLabelExt

Modification history

2023-09-19 01:45
Mathlib/Tactic/LabelAttr.lean
feat: update to leanprover/std4#258 (#7248)
Deleted Mathlib.Tactic.LabelAttr.mkLabelExtView on Github →
2023-02-13 18:09
Mathlib/Tactic/LabelAttr.lean
chore: rename register_tag_attr, and explain relation to registerTagAttribute (#2124) …
Added Mathlib.Tactic.LabelAttr.mkLabelExtView on Github →