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.UnicodeVariant.emoji : Char

Following any unicode character, this indicates that the emoji variant should be displayed

def Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.text : Char

Following any unicode character, this indicates that the text variant should be displayed

def Mathlib.Linter.TextBased.UnicodeLinter.Char.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.String.printCodepointHex (s : String) : String

Prints all characters in a string in hexadecimal with prefix 'U+'. E.g., "ab" is "U+0061;U+0062".

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

Blocklist: If false, the character is not allowed in Mathlib. Note: if true, a character might still not be allowed depending on context (e.g. misplaced variant selectors).

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

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

def Mathlib.Linter.TextBased.UnicodeLinter.emojis : Array Char

Unicode symbols in mathlib that should always be followed by the emoji variant selector.

def Mathlib.Linter.TextBased.UnicodeLinter.nonEmojis : Array Char

Unicode symbols in mathlib that should always be followed by the text variant selector.