mathlib3 documentation

core / init.data.array.basic

structure d_array (n : ) (α : fin n Type u) :
  • data : Π (i : fin n), α i

In the VM, d_array is implemented as a persistent array.

Instances for d_array
def d_array.nil {α : fin 0 Type u_1} :
d_array 0 α

The empty array.

Equations
def d_array.read {n : } {α : fin n Type u} (a : d_array n α) (i : fin n) :
α i

read a i reads the ith member of a. Has builtin VM implementation.

Equations
def d_array.write {n : } {α : fin n Type u} (a : d_array n α) (i : fin n) (v : α i) :
d_array n α

write a i v sets the ith member of a to be v. Has builtin VM implementation.

Equations
def d_array.iterate_aux {n : } {α : fin n Type u} {β : Type w} (a : d_array n α) (f : Π (i : fin n), α i β β) (i : ) :
i n β β
Equations
def d_array.iterate {n : } {α : fin n Type u} {β : Type w} (a : d_array n α) (b : β) (f : Π (i : fin n), α i β β) :
β

Fold over the elements of the given array in ascending order. Has builtin VM implementation.

Equations
def d_array.foreach {n : } {α : fin n Type u} {α' : fin n Type v} (a : d_array n α) (f : Π (i : fin n), α i α' i) :
d_array n α'

Map the array. Has builtin VM implementation.

Equations
def d_array.map {n : } {α : fin n Type u} {α' : fin n Type v} (f : Π (i : fin n), α i α' i) (a : d_array n α) :
d_array n α'
Equations
def d_array.map₂ {n : } {α : fin n Type u} {α' : fin n Type v} {α'' : fin n Type w} (f : Π (i : fin n), α i α' i α'' i) (a : d_array n α) (b : d_array n α') :
d_array n α''
Equations
def d_array.foldl {n : } {α : fin n Type u} {β : Type w} (a : d_array n α) (b : β) (f : Π (i : fin n), α i β β) :
β
Equations
def d_array.rev_iterate_aux {n : } {α : fin n Type u} {β : Type w} (a : d_array n α) (f : Π (i : fin n), α i β β) (i : ) :
i n β β
Equations
def d_array.rev_iterate {n : } {α : fin n Type u} {β : Type w} (a : d_array n α) (b : β) (f : Π (i : fin n), α i β β) :
β
Equations
@[simp]
theorem d_array.read_write {n : } {α : fin n Type u} (a : d_array n α) (i : fin n) (v : α i) :
(a.write i v).read i = v
@[simp]
theorem d_array.read_write_of_ne {n : } {α : fin n Type u} (a : d_array n α) {i j : fin n} (v : α i) :
i j (a.write i v).read j = a.read j
@[protected]
theorem d_array.ext {n : } {α : fin n Type u} {a b : d_array n α} (h : (i : fin n), a.read i = b.read i) :
a = b
@[protected]
theorem d_array.ext' {n : } {α : fin n Type u} {a b : d_array n α} (h : (i : ) (h : i < n), a.read i, h⟩ = b.read i, h⟩) :
a = b
@[protected]
def d_array.beq_aux {n : } {α : fin n Type u} [Π (i : fin n), decidable_eq (α i)] (a b : d_array n α) (i : ) :
Equations
@[protected]
def d_array.beq {n : } {α : fin n Type u} [Π (i : fin n), decidable_eq (α i)] (a b : d_array n α) :

Boolean element-wise equality check.

Equations
theorem d_array.of_beq_aux_eq_tt {n : } {α : fin n Type u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} (i : ) (h : i n) :
a.beq_aux b i h = bool.tt (j : ) (h' : j < i), a.read j, _⟩ = b.read j, _⟩
theorem d_array.of_beq_eq_tt {n : } {α : fin n Type u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} :
a.beq b = bool.tt a = b
theorem d_array.of_beq_aux_eq_ff {n : } {α : fin n Type u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} (i : ) (h : i n) :
a.beq_aux b i h = bool.ff ( (j : ) (h' : j < i), a.read j, _⟩ b.read j, _⟩)
theorem d_array.of_beq_eq_ff {n : } {α : fin n Type u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} :
a.beq b = bool.ff a b
@[protected, instance]
def d_array.decidable_eq {n : } {α : fin n Type u} [Π (i : fin n), decidable_eq (α i)] :
Equations
def array (n : ) (α : Type u) :

A non-dependent array (see d_array). Implemented in the VM as a persistent array.

Equations
Instances for array
def mk_array {α : Type u_1} (n : ) (v : α) :
array n α

mk_array n v creates a new array of length n where each element is v. Has builtin VM implementation.

Equations
def array.nil {α : Type u_1} :
array 0 α
Equations
def array.read {n : } {α : Type u} (a : array n α) (i : fin n) :
α
Equations
def array.write {n : } {α : Type u} (a : array n α) (i : fin n) (v : α) :
array n α
Equations
def array.iterate {n : } {α : Type u} {β : Type v} (a : array n α) (b : β) (f : fin n α β β) :
β

Fold array starting from 0, folder function includes an index argument.

Equations
def array.foreach {n : } {α : Type u} {β : Type v} (a : array n α) (f : fin n α β) :
array n β

Map each element of the given array with an index argument.

Equations
def array.map₂ {n : } {α : Type u} (f : α α α) (a b : array n α) :
array n α
Equations
def array.foldl {n : } {α : Type u} {β : Type v} (a : array n α) (b : β) (f : α β β) :
β
Equations
def array.rev_list {n : } {α : Type u} (a : array n α) :
list α
Equations
def array.rev_iterate {n : } {α : Type u} {β : Type v} (a : array n α) (b : β) (f : fin n α β β) :
β
Equations
def array.rev_foldl {n : } {α : Type u} {β : Type v} (a : array n α) (b : β) (f : α β β) :
β
Equations
def array.to_list {n : } {α : Type u} (a : array n α) :
list α
Equations
theorem array.push_back_idx {j n : } (h₁ : j < n + 1) (h₂ : j n) :
j < n
def array.push_back {n : } {α : Type u} (a : array n α) (v : α) :
array (n + 1) α

push_back a v pushes value v to the end of the array. Has builtin VM implementation.

Equations
  • a.push_back v = {data := λ (_x : fin (n + 1)), array.push_back._match_1 a v _x}
  • array.push_back._match_1 a v j, h₁⟩ = dite (j = n) (λ (h₂ : j = n), v) (λ (h₂ : ¬j = n), a.read j, _⟩)
theorem array.pop_back_idx {j n : } (h : j < n) :
j < n + 1
def array.pop_back {n : } {α : Type u} (a : array (n + 1) α) :
array n α

Discard last element in the array. Has builtin VM implementation.

Equations
def array.mmap_core {n : } {α : Type u} {β : Type v} {m : Type v Type w} [monad m] (a : array n α) (f : α m β) (i : ) (H : i n) :
m (array i β)

Auxilliary function for monadically mapping a function over an array.

Equations
def array.mmap {n : } {α : Type u} {β : Type v} {m : Type v Type u_1} [monad m] (a : array n α) (f : α m β) :
m (array n β)

Monadically map a function over the array.

Equations
def array.map {n : } {α : Type u} {β : Type v} (a : array n α) (f : α β) :
array n β

Map a function over the array.

Equations
@[protected]
def array.mem {n : } {α : Type u} (v : α) (a : array n α) :
Prop
Equations
@[protected, instance]
def array.has_mem {n : } {α : Type u} :
has_mem α (array n α)
Equations
theorem array.read_mem {n : } {α : Type u} (a : array n α) (i : fin n) :
a.read i a
@[protected, instance]
def array.has_repr {n : } {α : Type u} [has_repr α] :
Equations
@[protected, instance]
meta def array.has_to_format {n : } {α : Type u} [has_to_format α] :
@[protected, instance]
@[simp]
theorem array.read_write {n : } {α : Type u} (a : array n α) (i : fin n) (v : α) :
(a.write i v).read i = v
@[simp]
theorem array.read_write_of_ne {n : } {α : Type u} (a : array n α) {i j : fin n} (v : α) :
i j (a.write i v).read j = a.read j
def array.read' {n : } {β : Type v} [inhabited β] (a : array n β) (i : ) :
β
Equations
def array.write' {n : } {α : Type u} (a : array n α) (i : ) (v : α) :
array n α
Equations
theorem array.read_eq_read' {n : } {α : Type u} [inhabited α] (a : array n α) {i : } (h : i < n) :
a.read i, h⟩ = a.read' i
theorem array.write_eq_write' {n : } {α : Type u} (a : array n α) {i : } (h : i < n) (v : α) :
a.write i, h⟩ v = a.write' i v
@[protected, ext]
theorem array.ext {n : } {α : Type u} {a b : array n α} (h : (i : fin n), a.read i = b.read i) :
a = b
@[protected]
theorem array.ext' {n : } {α : Type u} {a b : array n α} (h : (i : ) (h : i < n), a.read i, h⟩ = b.read i, h⟩) :
a = b
@[protected, instance]
def array.decidable_eq {n : } {α : Type u} [decidable_eq α] :
Equations