mathlib documentation

core / init.data.array.basic

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

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

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

The empty array.

Equations
def d_array.read {n : } {α : fin nType 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 nType 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 nType u} {β : Type w} (a : d_array n α) (f : Π (i : fin n), α iβ → β) (i : ) :
i nβ → β
Equations
def d_array.iterate {n : } {α : fin nType 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 nType u} {α' : fin nType 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 nType u} {α' : fin nType v} (f : Π (i : fin n), α iα' i) (a : d_array n α) :
d_array n α'
Equations
def d_array.map₂ {n : } {α : fin nType u} {α' : fin nType v} {α'' : fin nType 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 nType u} {β : Type w} (a : d_array n α) (b : β) (f : Π (i : fin n), α iβ → β) :
β
Equations
def d_array.rev_iterate_aux {n : } {α : fin nType u} {β : Type w} (a : d_array n α) (f : Π (i : fin n), α iβ → β) (i : ) :
i nβ → β
Equations
def d_array.rev_iterate {n : } {α : fin nType u} {β : Type w} (a : d_array n α) (b : β) (f : Π (i : fin n), α iβ → β) :
β
Equations
@[simp]
theorem d_array.read_write {n : } {α : fin nType 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 nType 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 nType 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 nType 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 nType u} [Π (i : fin n), decidable_eq (α i)] (a b : d_array n α) (i : ) :
i nbool
Equations
@[protected]
def d_array.beq {n : } {α : fin nType 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 nType u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} (i : ) (h : i n) :
a.beq_aux b i h = tt∀ (j : ) (h' : j < i), a.read j, _⟩ = b.read j, _⟩
theorem d_array.of_beq_eq_tt {n : } {α : fin nType u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} :
a.beq b = tta = b
theorem d_array.of_beq_aux_eq_ff {n : } {α : fin nType u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} (i : ) (h : i n) :
a.beq_aux b i h = ff(∃ (j : ) (h' : j < i), a.read j, _⟩ b.read j, _⟩)
theorem d_array.of_beq_eq_ff {n : } {α : fin nType u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} :
a.beq b = ffa b
@[protected, instance]
def d_array.decidable_eq {n : } {α : fin nType u} [Π (i : fin n), decidable_eq (α i)] :
Equations
def array (n : ) (α : Type u) :
Type u

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

Equations
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 vType 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 vType 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]
meta def array.has_to_tactic_format {n : } {α : Type u} [has_to_tactic_format α] :
@[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