Tools for the unicode Linter

The actual linter is defined in TextBased.lean.

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

When changing, make sure to stay in sync with style guide

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

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

If false, the character is not allowed in Mathlib.

Implemented using an allowlist consisting of:

• certain ASCII characters
• characters with abbreviations in the VSCode extension (withVSCodeAbbrev)
• "the rest" (othersInMathlib)

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 disallowed character, or none if none defined