Def Char.isAscii

Modification history

2026-04-13 16:58
Mathlib/Data/String/Defs.lean
feat(Tactic/Linter): lint unwanted unicode (#36773) …
Added Char.isAsciiView on Github →