Documentation

Init.Data.Array.DecidableEq

@[irreducible]
theorem Array.eq_of_isEqvAux {α : Type u_1} [DecidableEq α] (a : Array α) (b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i a.size) (heqv : a.isEqvAux b hsz (fun (x y : α) => decide (x = y)) i = true) (j : Nat) (low : i j) (high : j < a.size) :
a[j] = b[j]
theorem Array.eq_of_isEqv {α : Type u_1} [DecidableEq α] (a : Array α) (b : Array α) :
(a.isEqv b fun (x y : α) => decide (x = y)) = truea = b
@[irreducible]
theorem Array.isEqvAux_self {α : Type u_1} [DecidableEq α] (a : Array α) (i : Nat) :
a.isEqvAux a (fun (x y : α) => decide (x = y)) i = true
theorem Array.isEqv_self {α : Type u_1} [DecidableEq α] (a : Array α) :
(a.isEqv a fun (x y : α) => decide (x = y)) = true
instance Array.instDecidableEq {α : Type u_1} [DecidableEq α] :
Equations