Documentation

Mathlib.Tactic.Linter.TextBased.UnicodeLinter

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.

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

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

            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