Documentation

Init.Data.Array.Mem

theorem List.sizeOf_get_lt {α : Type u_1} [inst : SizeOf α] (as : List α) (i : Fin (List.length as)) :
instance Array.instMembershipArray {α : Type u_1} [inst : DecidableEq α] :
Equations
theorem Array.sizeOf_get_lt {α : Type u_1} [inst : SizeOf α] (as : Array α) (i : Fin (Array.size as)) :
theorem Array.sizeOf_lt_of_mem {α : Type u_1} {a : α} [inst : DecidableEq α] [inst : SizeOf α] {as : Array α} (h : a as) :
theorem Array.sizeOf_lt_of_mem.aux {α : Type u_1} {a : α} [inst : DecidableEq α] [inst : SizeOf α] {as : Array α} (h : Array.anyM.loop (fun b => decide (a = b)) as (Array.size as) (_ : Array.size as Array.size as) 0 = true) (j : Nat) (h : Array.anyM.loop (fun b => decide (a = b)) as (Array.size as) (_ : Array.size as Array.size as) j = true) :
@[simp]
theorem Array.sizeOf_get {α : Type u_1} [inst : SizeOf α] (as : Array α) (i : Fin (Array.size as)) :