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 : Char) (b : Char) :
    Equations
    • a.lt b = (a.val < b.val)
    Instances For
      def Char.le (a : Char) (b : Char) :
      Equations
      • a.le b = (a.val b.val)
      Instances For
        instance Char.instLT :
        Equations
        instance Char.instLE :
        Equations
        instance Char.instDecidableLt (a : Char) (b : Char) :
        Decidable (a < b)
        Equations
        • a.instDecidableLt b = a.val.decLt b.val
        instance Char.instDecidableLe (a : Char) (b : Char) :
        Equations
        • a.instDecidableLe b = a.val.decLe b.val
        @[reducible, inline]

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

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

          Underlying unicode code point as a Nat.

          Equations
          • c.toNat = c.val.toNat
          Instances For
            @[inline]

            Convert a character into a UInt8, by truncating (reducing modulo 256) if necessary.

            Equations
            • c.toUInt8 = c.val.toUInt8
            Instances For

              The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other.

              Equations
              Instances For
                Equations
                @[inline]

                Is the character a space (U+0020) a tab (U+0009), a carriage return (U+000D) or a newline (U+000A)?

                Equations
                Instances For
                  @[inline]

                  Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZ?

                  Equations
                  Instances For
                    @[inline]

                    Is the character in abcdefghijklmnopqrstuvwxyz?

                    Equations
                    Instances For
                      @[inline]

                      Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz?

                      Equations
                      • c.isAlpha = (c.isUpper || c.isLower)
                      Instances For
                        @[inline]

                        Is the character in 0123456789?

                        Equations
                        Instances For
                          @[inline]

                          Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789?

                          Equations
                          • c.isAlphanum = (c.isAlpha || c.isDigit)
                          Instances For

                            Convert an upper case character to its lower case character.

                            Only works on basic latin letters.

                            Equations
                            Instances For

                              Convert a lower case character to its upper case character.

                              Only works on basic latin letters.

                              Equations
                              Instances For