structure Array.Mem {α : Type u_1} (as : Array α) (a : α) : Prop

a ∈ as is a predicate which asserts that a is in the array as.

• val : a ∈ as.toList

theorem Array.Mem.val {α : Type u_1} {as : Array α} {a : α} (self : as.Mem a) : a ∈ as.toList

instance Array.instMembership {α : Type u_1} : Membership α (Array α)

Equations

• Array.instMembership = { mem := Array.Mem }

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

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

@[simp]

theorem Array.sizeOf_getElem {α : Type u_1} [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf 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)

def Array.tacticArray_mem_dec : Lean.ParserDescr

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

Equations

• Array.tacticArray_mem_dec = Lean.ParserDescr.node `Array.tacticArray_mem_dec 1024 (Lean.ParserDescr.nonReservedSymbol "array_mem_dec" false)