theorem List.sizeOf_get_lt {α : Type u_1} [SizeOf α] (as : List α) (i : Fin (List.length as)) : sizeOf (List.get as i) < sizeOf as

instance Array.instMembershipArray {α : Type u_1} [DecidableEq α] : Membership α (Array α)

Equations

• Array.instMembershipArray = { mem := fun a as => Array.contains as a = true }

theorem Array.sizeOf_get_lt {α : Type u_1} [SizeOf α] (as : Array α) (i : Fin (Array.size as)) : sizeOf (Array.get as i) < sizeOf as

theorem Array.sizeOf_lt_of_mem {α : Type u_1} {a : α} [DecidableEq α] [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as

theorem Array.sizeOf_lt_of_mem.aux {α : Type u_1} {a : α} [DecidableEq α] [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) : sizeOf a < sizeOf as

@[simp]

theorem Array.sizeOf_get {α : Type u_1} [SizeOf α] (as : Array α) (i : Fin (Array.size as)) : sizeOf (Array.get as i) < sizeOf as

def Array.tacticArray_get_dec : Lean.ParserDescr

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf arr[i] < sizeOf arr, which is useful for well founded recursions over a nested inductive like inductive T | mk : Array T → T.

Equations

• Array.tacticArray_get_dec = Lean.ParserDescr.node `Array.tacticArray_get_dec 1024 (Lean.ParserDescr.nonReservedSymbol "array_get_dec" false)