Documentation

Init.Data.Array.Mem

source
theorem Array.sizeOf_lt_of_mem {α : Type u_1} {a : α} [SizeOf α] {as : Array α} (h : a ∈ as) :
sizeOf a < sizeOf as
source
theorem Array.sizeOf_get {α : Type u_1} [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
sizeOf (as.get i h) < sizeOf as
source
@[simp]
theorem Array.sizeOf_getElem {α : Type u_1} [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
sizeOf as[i] < sizeOf as
source
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
Instances For
    source
    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
    Instances For