theorem
List.sizeOf_get_lt
{α : Type u_1}
[inst : SizeOf α]
(as : List α)
(i : Fin (List.length as))
:
Equations
- Array.instMembershipArray = { mem := fun a as => Array.contains as a = true }
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))
:
Equations
- Array.tacticArray_get_dec = Lean.ParserDescr.node `Array.tacticArray_get_dec 1024 (Lean.ParserDescr.nonReservedSymbol "array_get_dec" false)