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".

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

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

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

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