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

theorem Vector.isEqv_eq_decide {α : Type u_1} {n : Nat} (xs ys : Vector α n) (r : α → α → Bool) : xs.isEqv ys r = decide (∀ (i : Nat) (h' : i < n), r xs[i] ys[i] = true)

@[simp]

theorem Vector.isEqv_toArray {α : Type u_1} {n : Nat} {r : α → α → Bool} [BEq α] (xs ys : Vector α n) : xs.isEqv ys.toArray r = xs.isEqv ys r

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

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

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

instance Vector.instDecidableEq {α : Type u_1} {n : Nat} [DecidableEq α] : DecidableEq (Vector α n)

Equations

• xs.instDecidableEq ys = match h : xs.isEqv ys fun (x y : α) => decide (x = y) with | true => isTrue ⋯ | false => isFalse ⋯

theorem Vector.beq_eq_decide {α : Type u_1} {n : Nat} [BEq α] (xs ys : Vector α n) : (xs == ys) = decide (∀ (i : Nat) (h' : i < n), (xs[i] == ys[i]) = true)

@[simp]

theorem Vector.beq_mk {α : Type u_1} {n : Nat} [BEq α] (xs ys : Array α) (ha : xs.size = n) (hb : ys.size = n) : ({ toArray := xs, size_toArray := ha } == { toArray := ys, size_toArray := hb }) = (xs == ys)

@[simp]

theorem Vector.beq_toArray {α : Type u_1} {n : Nat} [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys)

@[simp]

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

instance Vector.instLawfulBEq {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] : LawfulBEq (Vector α n)