Documentation

Batteries.Data.Char.AsciiCasing

Lemmas for ASCII-casing #

These facts apply for ASCII characters only. Recall that isAlpha, isLower, isUpper, toLower, toUpper do not consider characters outside the ASCII character range (code points less than 128).

source
theorem Char.not_isLower_of_isUpper {c : Char} :
c.isUpper = true → ¬c.isLower = true
source
theorem Char.not_isUpper_of_isLower {c : Char} :
c.isLower = true → ¬c.isUpper = true
source
theorem Char.toLower_eq_of_not_isUpper {c : Char} (h : ¬c.isUpper = true) :
c.toLower = c
source
theorem Char.toLower_eq_of_isUpper {c : Char} (h : c.isUpper = true) :
c.toLower = ofNat (c.toNat + 32)
source
theorem Char.toUpper_eq_of_not_isLower {c : Char} (h : ¬c.isLower = true) :
c.toUpper = c
source
theorem Char.toUpper_eq_of_isLower {c : Char} (h : c.isLower = true) :
c.toUpper = ofNat (c.toNat - 32)
source
@[simp]
theorem Char.isUpper_toLower_eq_false (c : Char) :
c.toLower.isUpper = false
source
@[simp]
theorem Char.isLower_toUpper_eq_false (c : Char) :
c.toUpper.isLower = false
source
@[simp]
theorem Char.isLower_toLower_eq_isAlpha (c : Char) :
c.toLower.isLower = c.isAlpha
source
@[simp]
theorem Char.isUpper_toUpper_eq_isAlpha (c : Char) :
c.toUpper.isUpper = c.isAlpha
source
@[simp]
theorem Char.isAlpha_toLower_eq_isAlpha (c : Char) :
c.toLower.isAlpha = c.isAlpha
source
@[simp]
theorem Char.isAlpha_toUpper_eq_isAlpha (c : Char) :
c.toUpper.isAlpha = c.isAlpha
source
@[simp]
theorem Char.toLower_toLower_eq_toLower (c : Char) :
c.toLower.toLower = c.toLower
source
@[simp]
theorem Char.toLower_toUpper_eq_toLower (c : Char) :
c.toUpper.toLower = c.toLower
source
@[simp]
theorem Char.toUpper_toUpper_eq_toUpper (c : Char) :
c.toUpper.toUpper = c.toUpper
source
@[simp]
theorem Char.toUpper_toLower_eq_toUpper (c : Char) :
c.toLower.toUpper = c.toUpper
source
@[reducible, inline]
abbrev Char.caseFoldAsciiOnly (c : Char) :
Char

Case folding for ASCII characters only.

Alphabetic ASCII characters are mapped to their lowercase form, all other characters are left unchanged. This agrees with the Unicode case folding algorithm for ASCII characters.

#eval caseFoldAsciiOnly 'A' == 'a'
#eval caseFoldAsciiOnly 'a' == 'a'
#eval caseFoldAsciiOnly 'À' == 'À'
#eval caseFoldAsciiOnly 'à' == 'à'
#eval caseFoldAsciiOnly '$' == '$'
Equations
Instances For
    source
    def Char.beqCaseInsensitiveAsciiOnly (c₁ c₂ : Char) :
    Bool

    Bool-valued comparison of two Chars for ASCII-case insensitive equality.

    #eval beqCaseInsensitiveAsciiOnly 'a' 'A' -- true
#eval beqCaseInsensitiveAsciiOnly 'a' 'a' -- true
#eval beqCaseInsensitiveAsciiOnly '$' '$' -- true
#eval beqCaseInsensitiveAsciiOnly 'a' 'b' -- false
#eval beqCaseInsensitiveAsciiOnly 'γ' 'Γ' -- false
#eval beqCaseInsensitiveAsciiOnly 'ä' 'Ä' -- false
    Equations
    Instances For
      source
      theorem Char.beqCaseInsensitiveAsciiOnly.eqv :
      Equivalence fun (x1 x2 : Char) => x1.beqCaseInsensitiveAsciiOnly x2 = true
      source
      def Char.beqCaseInsensitiveAsciiOnly.isSetoid :
      Setoid Char

      Setoid structure on Char using beqCaseInsensitiveAsciiOnly

      Equations
      Instances For
        source
        def Char.cmpCaseInsensitiveAsciiOnly (c₁ c₂ : Char) :
        Ordering

        ASCII-case insensitive implementation comparison returning an Ordering. Useful for sorting.

        #eval cmpCaseInsensitiveAsciiOnly 'a' 'A' -- eq
#eval cmpCaseInsensitiveAsciiOnly 'a' 'a' -- eq
#eval cmpCaseInsensitiveAsciiOnly '$' '$' -- eq
#eval cmpCaseInsensitiveAsciiOnly 'a' 'b' -- lt
#eval cmpCaseInsensitiveAsciiOnly 'γ' 'Γ' -- gt
#eval cmpCaseInsensitiveAsciiOnly 'ä' 'Ä' -- gt
        Equations
        Instances For