Documentation

Init.Data.Char.Basic

@[reducible, inline]

Determines if the given integer is a valid Unicode scalar value.

Note that values in [0xd800, 0xdfff] are reserved for UTF-16 surrogate pairs.

Equations
    Instances For
      def Char.lt (a b : Char) :

      One character is less than another if its code point is strictly less than the other's.

      Equations
        Instances For
          def Char.le (a b : Char) :

          One character is less than or equal to another if its code point is less than or equal to the other's.

          Equations
            Instances For
              instance Char.instLT :
              Equations
                instance Char.instLE :
                Equations
                  instance Char.instDecidableLt (a b : Char) :
                  Decidable (a < b)
                  Equations
                    instance Char.instDecidableLe (a b : Char) :
                    Equations
                      @[reducible, inline]

                      True for natural numbers that are valid Unicode scalar values.

                      Equations
                        Instances For
                          @[inline]
                          def Char.toNat (c : Char) :

                          The character's Unicode code point as a Nat.

                          Equations
                            Instances For
                              @[inline]

                              Converts a character into a UInt8 that contains its code point.

                              If the code point is larger than 255, it is truncated (reduced modulo 256).

                              Equations
                                Instances For

                                  Converts an 8-bit unsigned integer into a character.

                                  The integer's value is interpreted as a Unicode code point.

                                  Equations
                                    Instances For
                                      @[inline]

                                      Returns true if the character is a space (' ', U+0020), a tab ('\t', U+0009), a carriage return ('\r', U+000D), or a newline ('\n', U+000A).

                                      Equations
                                        Instances For
                                          @[inline]

                                          Returns true if the character is a uppercase ASCII letter.

                                          The uppercase ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZ.

                                          Equations
                                            Instances For
                                              @[inline]

                                              Returns true if the character is a lowercase ASCII letter.

                                              The lowercase ASCII letters are the following: abcdefghijklmnopqrstuvwxyz.

                                              Equations
                                                Instances For
                                                  @[inline]

                                                  Returns true if the character is an ASCII letter.

                                                  The ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz.

                                                  Equations
                                                    Instances For
                                                      @[inline]

                                                      Returns true if the character is an ASCII digit.

                                                      The ASCII digits are the following: 0123456789.

                                                      Equations
                                                        Instances For
                                                          @[inline]

                                                          Returns true if the character is an ASCII letter or digit.

                                                          The ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz. The ASCII digits are the following: 0123456789.

                                                          Equations
                                                            Instances For

                                                              Converts an uppercase ASCII letter to the corresponding lowercase letter. Letters outside the ASCII alphabet are returned unchanged.

                                                              The uppercase ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZ.

                                                              Equations
                                                                Instances For

                                                                  Converts a lowercase ASCII letter to the corresponding uppercase letter. Letters outside the ASCII alphabet are returned unchanged.

                                                                  The lowercase ASCII letters are the following: abcdefghijklmnopqrstuvwxyz.

                                                                  Equations
                                                                    Instances For