Bootstrapping theorems about arrays #
This file contains some theorems about Array
and List
needed for Init.Data.List.Impl
.
@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
Use the indexing notation a[i]
instead.
Access an element from an array without needing a runtime bounds checks,
using a Nat
index and a proof that it is in bounds.
This function does not use get_elem_tactic
to automatically find the proof that
the index is in bounds. This is because the tactic itself needs to look up values in
arrays.
Instances For
@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17")]
Use the indexing notation a[i]!
instead.
Access an element from an array, or panic if the index is out of bounds.
Instances For
@[simp]
theorem
Array.foldl_toList
{β : Type u_1}
{α : Type u_2}
(f : β → α → β)
{init : β}
{xs : Array α}
:
@[simp]
theorem
Array.foldr_toList
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
{init : β}
{xs : Array α}
:
@[reducible, inline, deprecated Array.toList_push (since := "2025-05-26")]
Equations
Instances For
@[simp]
@[reducible, inline, deprecated Array.toList_pop (since := "2025-02-17")]
Equations
Instances For
@[reducible, inline, deprecated Array.append_empty (since := "2025-01-13")]
Equations
Instances For
@[reducible, inline, deprecated Array.empty_append (since := "2025-01-13")]
Equations
Instances For
@[simp]
@[reducible, inline, deprecated Array.toList_appendList (since := "2024-12-11")]