Documentation

Init.Data.Array.Mem

source
theorem List.sizeOf_get_lt {α : Type u_1} [SizeOf α] (as : List α) (i : Fin (List.length as)) :
sizeOf (List.get as i) < sizeOf as
source
structure Array.Mem {α : Type u_1} (a : α) (as : Array α) :
Prop

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

  • val : a ∈ as.data
Instances For
    source
    instance Array.instMembershipArray {α : Type u_1} :
    Membership α (Array α)
    Equations
    • Array.instMembershipArray = { mem := fun (a : α) (as : Array α) => Array.Mem a as }
    source
    theorem Array.sizeOf_get_lt {α : Type u_1} [SizeOf α] (as : Array α) (i : Fin (Array.size as)) :
    sizeOf (Array.get as i) < sizeOf as
    source
    theorem Array.sizeOf_lt_of_mem {α : Type u_1} {a : α} [SizeOf α] {as : Array α} (h : a ∈ as) :
    sizeOf a < sizeOf as
    source
    @[simp]
    theorem Array.sizeOf_get {α : Type u_1} [SizeOf α] (as : Array α) (i : Fin (Array.size as)) :
    sizeOf (Array.get 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