Mathlib Changelog
v4
Changelog
About
Github
Def
isPrivateUseAreaChar
Modification history
2026-04-13 16:58
MathlibTest/LintStyle.lean
feat(Tactic/Linter): lint unwanted unicode (#36773) …
Added
isPrivateUseAreaChar
View on Github →