Documentation

UnicodeBasic.Types

unsafe def Char.mkUnsafe :

Low-level conversion from UInt32 to Char (unsafe)

This function translates to a no-op in the compiler. However, it does not check whether the UInt32 code is a valid Char value. Only use where it's known for external reasons that the code is valid.

Instances For

    Coercion from String to Substring

    This coercion is in Batteries but not in Lean. It is scoped to Unicode here to avoid issues in low-level packages that don't use Batteries.

    Equations
    Instances For

      Maximum valid code point value

      Equations
      Instances For

        Hexadecimal string representation of a code point

        Same as toHexString but without the U+ prefix.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[inline]

          Hexadecimal string representation of a code point

          Prefix U+ followed by at least four uppercase hexadecimal digits (e.g. U+0123 and U+4B0A1 but neither U+123 nor U+4b0a1).

          Equations
          Instances For

            Get code point from hexadecimal string representation

            For convenience, the U+ prefix may be omitted and lowercase hexadecimal digits are accepted.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]

              Get value of hex digit

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Get code point from hexadecimal string representation

                For convenience, the U+ prefix may be omitted and lowercase hexadecimal digits are accepted.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  General Category #

                  Major general category (L, M, N, P, S, Z, C)

                  Unicode property: General_Category

                  Instances For

                    Minor general category

                    Unicode property: General_Category

                    Instances For
                      Equations
                      • Unicode.instDecidableEqMinorGeneralCategory = Unicode.decEqMinorGeneralCategory✝

                      General category of a code point

                      Unicode property: General_Category

                      Instances For
                        Equations

                        General category: letter (L)

                        Equations
                        Instances For

                          General category mark (M)

                          Equations
                          Instances For

                            General category: number (N)

                            Equations
                            Instances For

                              General category: punctuation (P)

                              Equations
                              Instances For

                                General category: symbol (S)

                                Equations
                                Instances For

                                  General category: separator (Z)

                                  Equations
                                  Instances For

                                    General category: other (C)

                                    Equations
                                    Instances For

                                      String abbreviation for general category

                                      Instances For

                                        Get general category from string abbreviation

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Get general category from string abbreviation

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.

                                            Numeric Type and Value #

                                            Unicode numeric type

                                            Unicode properties: Numeric_Type, Numeric_Value

                                            Instances For

                                              Decimal digit type

                                              The character is part of a sequence of contiguous code points representing decimal digits 0 through 9.

                                              Unicode property: Numeric_Type

                                              Equations
                                              Instances For

                                                Digit type

                                                The character represents a decimal digit 0 through 9.

                                                Unicode property: Numeric_Type

                                                Equations
                                                Instances For

                                                  Get the value of a numeric type

                                                  Returns either an integer value or a numerator-denominator pair representing a rational value.

                                                  Unicode property: Numeric_Value

                                                  Equations
                                                  Instances For

                                                    Decomposition Mapping #

                                                    Compatibility format tag

                                                    Unicode properties: Decomposition_Type, Decomposition_Mapping

                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.

                                                      Decomposition maping

                                                      Unicode properties: Decomposition_Type, Decomposition_Mapping

                                                      Instances For

                                                        Bidirectional Class #

                                                        Bidirectional class

                                                        Unicode property: Bidi_Class

                                                        Instances For
                                                          Equations

                                                          Bidi class: strong left-to-right (L)

                                                          Equations
                                                          Instances For

                                                            Bidi class: strong right-to-left (R)

                                                            Equations
                                                            Instances For

                                                              Get bidi class from abbreviation

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For

                                                                Get bidi class from abbreviation

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations

                                                                  Structure for data from UnicodeData.txt

                                                                  Instances For
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.