Tools for the unicode Linter

The actual linter is defined in TextBased.lean.

This file defines the blocklist and other tools used by the linter.

def Mathlib.Linter.TextBased.UnicodeLinter.printCodepointHex (c : Char) : String

Prints a unicode character's codepoint in hexadecimal with prefix 'U+'. E.g., 'a' is "U+0061".

Equations

• Mathlib.Linter.TextBased.UnicodeLinter.printCodepointHex c = ("U+".append ("0000".drop (Nat.toDigits 16 c.val.toNat).length).toString).append (String.ofList (Nat.toDigits 16 c.val.toNat))

def Mathlib.Linter.TextBased.UnicodeLinter.isAllowedCharacter (c : Char) : Bool

Blocklist: If false, the character is not allowed in Mathlib.

Equations

• Mathlib.Linter.TextBased.UnicodeLinter.isAllowedCharacter c = !#[' '].contains c

def Mathlib.Linter.TextBased.UnicodeLinter.replaceDisallowed : Char → Option String

Provide default replacement (String) for a blocklisted character, or none if none defined

Equations

• Mathlib.Linter.TextBased.UnicodeLinter.replaceDisallowed ' ' = some " "
• Mathlib.Linter.TextBased.UnicodeLinter.replaceDisallowed x✝ = none