theorem List.mem_finRange {n : Nat} (x : Fin n) : x ∈ finRange n

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

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

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 Char.instDecidableForallOfDecidablePred_batteries (P : Char → Prop) [DecidablePred P] : Decidable (∀ (c : Char), P c)

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