Def Char.manuallyExcluded

Modification history

2026-04-13 16:58
scripts/extract-unique-nonascii.lean
feat(Tactic/Linter): lint unwanted unicode (#36773) …
Added Char.manuallyExcludedView on Github →