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

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

Returns true if p returns true for every Char.

Equations

• Char.all p = ((Nat.all 55296 fun (c : Nat) (h₁ : c < 55296) => p (Char.ofNatAux c ⋯)) && (1114112 - 57344).all fun (c : Nat) (h₂ : c < 1114112 - 57344) => p (Char.ofNatAux (c + 57344) ⋯))

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

• Char.any p = ((Nat.any 55296 fun (c : Nat) (h₁ : c < 55296) => p (Char.ofNatAux c ⋯)) || (1114112 - 57344).any fun (c : Nat) (h₂ : c < 1114112 - 57344) => p (Char.ofNatAux (c + 57344) ⋯))

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)