theorem Array.isEqv_iff_rel {α : Type u_1} {xs ys : Array α} {r : α → α → Bool} : xs.isEqv ys r = true ↔ ∃ (h : xs.size = ys.size), ∀ (i : Nat) (h' : i < xs.size), r xs[i] ys[i] = true

theorem Array.isEqv_eq_decide {α : Type u_1} (xs ys : Array α) (r : α → α → Bool) : xs.isEqv ys r = if h : xs.size = ys.size then decide (∀ (i : Nat) (h' : i < xs.size), r xs[i] ys[i] = true) else false

@[simp]

theorem Array.isEqv_toList {α : Type u_1} {r : α → α → Bool} [BEq α] (xs ys : Array α) : xs.toList.isEqv ys.toList r = xs.isEqv ys r

theorem Array.eq_of_isEqv {α : Type u_1} [DecidableEq α] (xs ys : Array α) (h : (xs.isEqv ys fun (x y : α) => decide (x = y)) = true) : xs = ys

theorem Array.isEqv_self_beq {α : Type u_1} [BEq α] [ReflBEq α] (xs : Array α) : (xs.isEqv xs fun (x1 x2 : α) => x1 == x2) = true

theorem Array.isEqv_self {α : Type u_1} [DecidableEq α] (xs : Array α) : (xs.isEqv xs fun (x1 x2 : α) => decide (x1 = x2)) = true

def Array.instDecidableEqImpl {α : Type u_1} [DecidableEq α] : DecidableEq (Array α)

Equations

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

@[implicit_reducible]

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

Equations

• { toList := [] }.instDecidableEq { toList := [] } = isTrue ⋯
• { toList := [] }.instDecidableEq { toList := head :: tail } = isFalse ⋯
• { toList := head :: tail }.instDecidableEq { toList := [] } = isFalse ⋯
• { toList := head :: tail }.instDecidableEq { toList := head_1 :: tail_1 } = { toList := head :: tail }.instDecidableEqImpl { toList := head_1 :: tail_1 }

@[csimp]

theorem Array.instDecidableEq_csimp : @instDecidableEq = @instDecidableEqImpl

@[implicit_reducible]

instance Array.instDecidableEqEmp {α : Type u_1} (xs : Array α) : Decidable (xs = #[])

Equality with #[] is decidable even if the underlying type does not have decidable equality.

Equations

• { toList := [] }.instDecidableEqEmp = isTrue ⋯
• { toList := head :: tail }.instDecidableEqEmp = isFalse ⋯

@[implicit_reducible]

instance Array.instDecidableEmpEq {α : Type u_1} (ys : Array α) : Decidable (#[] = ys)

Equality with #[] is decidable even if the underlying type does not have decidable equality.

Equations

• { toList := [] }.instDecidableEmpEq = isTrue ⋯
• { toList := head :: tail }.instDecidableEmpEq = isFalse ⋯

@[inline]

def Array.instDecidableEqEmpImpl {α : Type u_1} (xs : Array α) : Decidable (xs = #[])

Equations

• xs.instDecidableEqEmpImpl = decidable_of_iff (xs.isEmpty = true) ⋯

@[inline]

def Array.instDecidableEmpEqImpl {α : Type u_1} (xs : Array α) : Decidable (#[] = xs)

Equations

• xs.instDecidableEmpEqImpl = decidable_of_iff (xs.isEmpty = true) ⋯

@[csimp]

theorem Array.instDecidableEqEmp_csimp : @instDecidableEqEmp = @instDecidableEqEmpImpl

@[csimp]

theorem Array.instDecidableEmpEq_csimp : @instDecidableEmpEq = @instDecidableEmpEqImpl

theorem Array.beq_eq_decide {α : Type u_1} [BEq α] (xs ys : Array α) : (xs == ys) = if h : xs.size = ys.size then decide (∀ (i : Nat) (h' : i < xs.size), (xs[i] == ys[i]) = true) else false

@[simp]

theorem Array.beq_toList {α : Type u_1} [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys)

@[simp]

theorem List.isEqv_toArray {α : Type u_1} {r : α → α → Bool} [BEq α] (as bs : List α) : as.toArray.isEqv bs.toArray r = as.isEqv bs r

@[simp]

theorem List.beq_toArray {α : Type u_1} [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs)

instance Array.instReflBEq {α : Type u_1} [BEq α] [ReflBEq α] : ReflBEq (Array α)

instance Array.instLawfulBEq {α : Type u_1} [BEq α] [LawfulBEq α] : LawfulBEq (Array α)