Def Mathlib.Linter.TextBased.UnicodeLinter.withVSCodeAbbrev

Modification history

2026-04-13 16:58
Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean
feat(Tactic/Linter): lint unwanted unicode (#36773) …
Added Mathlib.Linter.TextBased.UnicodeLinter.withVSCodeAbbrevView on Github →