Def allLinterDefinedCharacterLists

Modification history

2026-04-13 16:58
MathlibTest/LintStyle.lean
feat(Tactic/Linter): lint unwanted unicode (#36773) …
Added allLinterDefinedCharacterListsView on Github →