Documentation

Mathlib.Tactic.Linter.TextBased.UnicodeLinter

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

source
def Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.emoji :
Char

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

Equations
Instances For
    source
    def Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.text :
    Char

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

    Equations
    Instances For
      source
      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".

      Equations
      Instances For
        source
        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".

        Equations
        Instances For
          source
          def Mathlib.Linter.TextBased.UnicodeLinter.emojis :
          Array Char

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Mathlib.Linter.TextBased.UnicodeLinter.nonEmojis :
            Array Char

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

            Equations
            Instances For
              source
              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).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Mathlib.Linter.TextBased.UnicodeLinter.replaceDisallowed :
                Char → Option String

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

                Equations
                Instances For