theorem Char.le_antisymm_iff {x y : Char} : x = y ↔ x ≤ y ∧ y ≤ x

instance Char.instLawfulOrd : Std.LawfulOrd Char

@[simp]

theorem Char.toNat_ofNatAux {n : Nat} (h : n.isValidChar) : (ofNatAux n h).toNat = n

theorem Char.toNat_ofNat (n : Nat) : (ofNat n).toNat = if n.isValidChar then n else 0

@[simp]

theorem Char.val_ofNat {n : Nat} (hn : n.isValidChar) : (ofNat n).val = UInt32.ofNat n

@[simp]

theorem Char.ofNat_toNat_eq_val {c : Char} : UInt32.ofNat c.toNat = c.val

@[reducible, inline]

abbrev Char.max : Nat

Maximum character code point. (See unicode scalar value.)

Equations

• Char.max = 1114111

@[reducible, inline]

abbrev Char.maxSurrogate : Nat

Maximum surrogate code point. (See unicode scalar value.)

Equations

• Char.maxSurrogate = 57343

@[reducible, inline]

abbrev Char.minSurrogate : Nat

Minimum surrogate code point. (See unicode scalar value.)

Equations

• Char.minSurrogate = 55296

@[reducible, inline]

abbrev Char.count : Nat

Number of valid character code points. (See unicode scalar value.)

Equations

• Char.count = Char.max - Char.maxSurrogate + Char.minSurrogate

theorem Char.toNat_le_max (c : Char) : c.toNat ≤ Char.max

theorem Char.toNat_not_surrogate (c : Char) : ¬(Char.minSurrogate ≤ c.toNat ∧ c.toNat ≤ Char.maxSurrogate)

@[implicit_reducible, inline]

def Char.isAscii (c : Char) : Bool

Checks whether a character is in the ASCII range, that is, its code point is less than 128.

Equations

• c.isAscii = decide (c.val < 128)

theorem Char.isAscii_iff_toNat_lt {c : Char} : c.isAscii = true ↔ c.toNat < 128

theorem Char.isAscii_of_isUpper {c : Char} (h : c.isUpper = true) : c.isAscii = true

theorem Char.isAscii_of_isLower {c : Char} (h : c.isLower = true) : c.isAscii = true

theorem Char.isAscii_of_isAlpha {c : Char} (h : c.isAlpha = true) : c.isAscii = true

theorem Char.isAscii_of_isDigit {c : Char} (h : c.isDigit = true) : c.isAscii = true

theorem Char.isAscii_of_isAlphanum {c : Char} (h : c.isAlphanum = true) : c.isAscii = true

theorem Char.isAscii_of_isWhitespace {c : Char} (h : c.isWhitespace = true) : c.isAscii = true

def Char.all (p : Char → Bool) : Bool

Returns true if p returns true for every Char.

Equations

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

theorem Char.eq_true_of_all_eq_true {p : Char → Bool} (h : Char.all p = true) (c : Char) : p c = true

theorem Char.exists_eq_false_of_all_eq_false {p : Char → Bool} (h : Char.all p = false) : ∃ (c : Char), p c = false

theorem Char.all_eq_true_iff_forall_eq_true {p : Char → Bool} : Char.all p = true ↔ ∀ (c : Char), p c = true

def Char.any (p : Char → Bool) : Bool

Returns true if p returns true for some Char.

Equations

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

theorem Char.exists_eq_true_of_any_eq_true {p : Char → Bool} (h : Char.any p = true) : ∃ (c : Char), p c = true

theorem Char.eq_false_of_any_eq_false {p : Char → Bool} (h : Char.any p = false) (c : Char) : p c = false

theorem Char.any_eq_true_iff_exists_eq_true {p : Char → Bool} : Char.any p = true ↔ ∃ (c : Char), p c = true

@[instance_reducible]

instance Char.instDecidableForallOfDecidablePred_batteries (P : Char → Prop) [DecidablePred P] : Decidable (∀ (c : Char), P c)

@[instance_reducible]

instance Char.instDecidableExistsOfDecidablePred_batteries (P : Char → Prop) [DecidablePred P] : Decidable (∃ (c : Char), P c)