Def Mathlib.Linter.TextBased.UnicodeLinter.ASCII.allowed

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.ASCII.allowedView on Github →