Def Mathlib.Linter.TextBased.UnicodeLinter.ASCII.allowedWhitespace

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