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.unrestricted :
              Array Char

              Unicode symbols in mathlib that have no restrictions on whether they are followed by a selector or which selector they are followed by.

              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
                • certain emojis (emojis)
                • certain non-emoji variants of emojifiable characters (nonEmojis)
                • certain characters with no selector restrictions (unrestricted)
                • 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