Documentation

Init.Data.Array.DecidableEq

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)) = truea = 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