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

instance Char.instLawfulOrd : Std.LawfulOrd Char

@[simp]

theorem Char.toNat_val (c : Char) : c.val.toNat = c.toNat

@[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.toNat_mk {v : UInt32} (h : v.isValidChar) : { val := v, valid := h }.toNat = v.toNat

@[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.)

@[reducible, inline]

abbrev Char.maxSurrogate : Nat

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

@[reducible, inline]

abbrev Char.minSurrogate : Nat

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

@[reducible, inline]

abbrev Char.count : Nat

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

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)

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

Returns true if p returns true for every Char.

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.

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

@[implicit_reducible]

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

@[implicit_reducible]

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