theorem Array.eq_of_isEqvAux {α : Type u_1} [DecidableEq α] (a : Array α) (b : Array α) (hsz : Array.size a = Array.size b) (i : Nat) (hi : i ≤ Array.size a) (heqv : Array.isEqvAux a b hsz (fun (x y : α) => decide (x = y)) i = true) (j : Nat) (low : i ≤ j) (high : j < Array.size a) : a[j] = b[j]

theorem Array.eq_of_isEqv {α : Type u_1} [DecidableEq α] (a : Array α) (b : Array α) : (Array.isEqv a b fun (x y : α) => decide (x = y)) = true → a = b

theorem Array.isEqvAux_self {α : Type u_1} [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a (_ : Array.size a = Array.size a) (fun (x y : α) => decide (x = y)) i = true

theorem Array.isEqv_self {α : Type u_1} [DecidableEq α] (a : Array α) : (Array.isEqv a a fun (x y : α) => decide (x = y)) = true

instance Array.instDecidableEqArray {α : Type u_1} [DecidableEq α] : DecidableEq (Array α)

Equations

• Array.instDecidableEqArray a b = match h : Array.isEqv a b fun (a b : α) => decide (a = b) with | true => isTrue (_ : a = b) | false => isFalse (_ : a = b → False)