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) :
α id_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} :
d_array n αβ → (Π (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} :
d_array n α(Π (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} :
(Π (i : fin n), α iα' i)d_array n αd_array n α'

Equations
def d_array.map₂ {n : } {α : fin nType u} {α' : fin nType v} {α'' : fin nType w} :
(Π (i : fin n), α iα' iα'' i)d_array n αd_array n α'd_array n α''

Equations
def d_array.foldl {n : } {α : fin nType u} {β : Type w} :
d_array n αβ → (Π (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} :
d_array n αβ → (Π (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

theorem d_array.ext {n : } {α : fin nType u} {a b : d_array n α} :
(∀ (i : fin n), a.read i = b.read i)a = b

theorem d_array.ext' {n : } {α : fin nType u} {a b : d_array n α} :
(∀ (i : ) (h : i < n), a.read i, h⟩ = b.read i, h⟩)a = b

def d_array.beq_aux {n : } {α : fin nType u} [Π (i : fin n), decidable_eq (α i)] (a b : d_array n α) (i : ) :
i nbool

Equations
def d_array.beq {n : } {α : fin nType u} [Π (i : fin n), decidable_eq (α i)] :
d_array n αd_array n αbool

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

@[instance]
def d_array.decidable_eq {n : } {α : fin nType u} [Π (i : fin n), decidable_eq (α i)] :

Equations
def array  :
Type uType u

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

Equations
def mk_array {α : Type u_1} (n : ) :
α → 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} :
array n αfin n → α

Equations
def array.write {n : } {α : Type u} :
array n αfin nα → array n α

Equations
def array.iterate {n : } {α : Type u} {β : Type v} :
array n αβ → (fin nα → β → β) → β

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

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

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

Equations
def array.map₂ {n : } {α : Type u} :
(α → α → α)array n αarray n αarray n α

Equations
def array.foldl {n : } {α : Type u} {β : Type v} :
array n αβ → (α → β → β) → β

Equations
def array.rev_list {n : } {α : Type u} :
array n αlist α

Equations
def array.rev_iterate {n : } {α : Type u} {β : Type v} :
array n αβ → (fin nα → β → β) → β

Equations
def array.rev_foldl {n : } {α : Type u} {β : Type v} :
array n αβ → (α → β → β) → β

Equations
def array.to_list {n : } {α : Type u} :
array n αlist α

Equations
theorem array.push_back_idx {j n : } :
j < n + 1j nj < n

def array.push_back {n : } {α : Type u} :
array n αα → 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 : } :
j < nj < n + 1

def array.pop_back {n : } {α : Type u} :
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 : ) :
i nm (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] :
array n α(α → m β)m (array n β)

Monadically map a function over the array.

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

Map a function over the array.

Equations
def array.mem {n : } {α : Type u} :
α → array n α → Prop

Equations
@[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

@[instance]
def array.has_repr {n : } {α : Type u} [has_repr α] :

Equations
@[instance]
meta def array.has_to_format {n : } {α : Type u} [has_to_format α] :

@[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 β] :
array n β → β

Equations
def array.write' {n : } {α : Type u} :
array n αα → 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

@[ext]
theorem array.ext {n : } {α : Type u} {a b : array n α} :
(∀ (i : fin n), a.read i = b.read i)a = b

theorem array.ext' {n : } {α : Type u} {a b : array n α} :
(∀ (i : ) (h : i < n), a.read i, h⟩ = b.read i, h⟩)a = b

@[instance]
def array.decidable_eq {n : } {α : Type u} [decidable_eq α] :

Equations