HepLean Documentation

Init.Data.Array.DecidableEq

theorem Array.rel_of_isEqvAux {α : Type u_1} {r : ααBool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i a.size) (heqv : a.isEqvAux b hsz r i hi = true) {j : Nat} (hj : j < i) :
r a[j] b[j] = true
theorem Array.isEqvAux_of_rel {α : Type u_1} {r : ααBool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i a.size) (w : ∀ (j : Nat) (hj : j < i), r a[j] b[j] = true) :
a.isEqvAux b hsz r i hi = true
theorem Array.rel_of_isEqv {α : Type u_1} {r : ααBool} {a b : Array α} :
a.isEqv b r = true∃ (h : a.size = b.size), ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
theorem Array.isEqv_iff_rel {α : Type u_1} (a b : Array α) (r : ααBool) :
a.isEqv b r = true ∃ (h : a.size = b.size), ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
theorem Array.isEqv_eq_decide {α : Type u_1} (a b : Array α) (r : ααBool) :
a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false
@[simp]
theorem Array.isEqv_toList {α : Type u_1} {r : ααBool} [BEq α] (a b : Array α) :
a.toList.isEqv b.toList r = a.isEqv b r
theorem Array.eq_of_isEqv {α : Type u_1} [DecidableEq α] (a b : Array α) (h : (a.isEqv b fun (x y : α) => decide (x = y)) = true) :
a = b
theorem Array.isEqvAux_self {α : Type u_1} (r : ααBool) (hr : ∀ (a : α), r a a = true) (a : Array α) (i : Nat) (h : i a.size) :
a.isEqvAux a r i h = true
theorem Array.isEqv_self_beq {α : Type u_1} [BEq α] [ReflBEq α] (a : Array α) :
(a.isEqv a fun (x1 x2 : α) => x1 == x2) = true
theorem Array.isEqv_self {α : Type u_1} [DecidableEq α] (a : Array α) :
(a.isEqv a fun (x1 x2 : α) => decide (x1 = x2)) = true
instance Array.instDecidableEq {α : Type u_1} [DecidableEq α] :
Equations
theorem Array.beq_eq_decide {α : Type u_1} [BEq α] (a b : Array α) :
(a == b) = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true) else false
@[simp]
theorem Array.beq_toList {α : Type u_1} [BEq α] (a b : Array α) :
(a.toList == b.toList) = (a == b)
@[simp]
theorem List.isEqv_toArray {α : Type u_1} {r : ααBool} [BEq α] (a b : List α) :
a.toArray.isEqv b.toArray r = a.isEqv b r
@[simp]
theorem List.beq_toArray {α : Type u_1} [BEq α] (a b : List α) :
(a.toArray == b.toArray) = (a == b)