@[reducible, inline]

abbrev String.caseFoldAsciiOnly (s : String) : String

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 "ABC".caseFoldAsciiOnly == "abc" -- true
#eval "x".caseFoldAsciiOnly == "y" -- false
#eval "Àà".caseFoldAsciiOnly == "Àà" -- true
#eval "1$#!".caseFoldAsciiOnly == "1$#!" -- true

Equations

• s.caseFoldAsciiOnly = String.map Char.caseFoldAsciiOnly s

@[implemented_by _private.Batteries.Data.String.AsciiCasing.0.String.beqCaseInsensitiveAsciiOnlyImpl]

def String.beqCaseInsensitiveAsciiOnly (s₁ s₂ : String) : Bool

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

#eval "abc".beqCaseInsensitiveAsciiOnly "ABC" -- true #eval "cba".beqCaseInsensitiveAsciiOnly "ABC" -- false #eval "$".beqCaseInsensitiveAsciiOnly "$" -- true #eval "a".beqCaseInsensitiveAsciiOnly "b" -- false #eval "γ".beqCaseInsensitiveAsciiOnly "Γ" -- false

Equations

• s₁.beqCaseInsensitiveAsciiOnly s₂ = (s₁.caseFoldAsciiOnly == s₂.caseFoldAsciiOnly)

theorem String.beqCaseInsensitiveAsciiOnly.eqv : Equivalence fun (x1 x2 : String) => x1.beqCaseInsensitiveAsciiOnly x2 = true

def String.beqCaseInsensitiveAsciiOnly.isSetoid : Setoid String

Setoid structure on String usig beqCaseInsensitiveAsciiOnly

Equations

• String.beqCaseInsensitiveAsciiOnly.isSetoid = { r := fun (x1 x2 : String) => x1.beqCaseInsensitiveAsciiOnly x2 = true, iseqv := String.beqCaseInsensitiveAsciiOnly.eqv }

@[implemented_by _private.Batteries.Data.String.AsciiCasing.0.String.cmpCaseInsensitiveAsciiOnlyImpl]

def String.cmpCaseInsensitiveAsciiOnly (s₁ s₂ : String) : 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

Equations

• s₁.cmpCaseInsensitiveAsciiOnly s₂ = compare s₁.caseFoldAsciiOnly s₂.caseFoldAsciiOnly