theorem Array.rel_of_isEqvAux {α : Type u_1} (r : α → α → Bool) (a : Array α) (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.rel_of_isEqv {α : Type u_1} (r : α → α → Bool) (a : Array α) (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.eq_of_isEqv {α : Type u_1} [DecidableEq α] (a : Array α) (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 α] : DecidableEq (Array α)

Equations

• a.instDecidableEq b = match h : a.isEqv b fun (a b : α) => decide (a = b) with | true => isTrue ⋯ | false => isFalse ⋯