mathlib3 documentation

data.buffer.basic

@[protected, instance]
def buffer.inhabited {α : Type u_1} :
Equations
@[ext]
theorem buffer.ext {α : Type u_1} {b₁ b₂ : buffer α} :
b₁.to_list = b₂.to_list b₁ = b₂
theorem buffer.ext_iff {α : Type u_1} {b₁ b₂ : buffer α} :
b₁ = b₂ b₁.to_list = b₂.to_list
theorem buffer.size_eq_zero_iff {α : Type u_1} {b : buffer α} :
@[simp]
theorem buffer.size_nil {α : Type u_1} :
@[simp]
@[protected, instance]
Equations
@[simp]
theorem buffer.to_list_append_list {α : Type u_1} {xs : list α} {b : buffer α} :
@[simp]
@[simp]
theorem buffer.to_buffer_to_list {α : Type u_1} (b : buffer α) :
@[simp]
theorem buffer.to_list_to_buffer {α : Type u_1} (l : list α) :
@[simp]
theorem buffer.to_list_to_array {α : Type u_1} (b : buffer α) :
@[simp]
theorem buffer.append_list_nil {α : Type u_1} (b : buffer α) :
theorem buffer.to_buffer_cons {α : Type u_1} (c : α) (l : list α) :
@[simp]
theorem buffer.size_push_back {α : Type u_1} (b : buffer α) (a : α) :
(b.push_back a).size = b.size + 1
@[simp]
theorem buffer.size_append_list {α : Type u_1} (b : buffer α) (l : list α) :
@[simp]
theorem buffer.size_to_buffer {α : Type u_1} (l : list α) :
@[simp]
theorem buffer.length_to_list {α : Type u_1} (b : buffer α) :
theorem buffer.size_singleton {α : Type u_1} (a : α) :
theorem buffer.read_push_back_left {α : Type u_1} (b : buffer α) (a : α) {i : } (h : i < b.size) :
(b.push_back a).read i, _⟩ = b.read i, h⟩
@[simp]
theorem buffer.read_push_back_right {α : Type u_1} (b : buffer α) (a : α) :
(b.push_back a).read b.size, _⟩ = a
theorem buffer.read_append_list_left' {α : Type u_1} (b : buffer α) (l : list α) {i : } (h : i < (b.append_list l).size) (h' : i < b.size) :
(b.append_list l).read i, h⟩ = b.read i, h'⟩
theorem buffer.read_append_list_left {α : Type u_1} (b : buffer α) (l : list α) {i : } (h : i < b.size) :
(b.append_list l).read i, _⟩ = b.read i, h⟩
@[simp]
theorem buffer.read_append_list_right {α : Type u_1} (b : buffer α) (l : list α) {i : } (h : i < l.length) :
(b.append_list l).read b.size + i, _⟩ = l.nth_le i h
theorem buffer.read_to_buffer' {α : Type u_1} (l : list α) {i : } (h : i < l.to_buffer.size) (h' : i < l.length) :
l.to_buffer.read i, h⟩ = l.nth_le i h'
@[simp]
theorem buffer.read_to_buffer {α : Type u_1} (l : list α) (i : fin l.to_buffer.size) :
theorem buffer.nth_le_to_list' {α : Type u_1} (b : buffer α) {i : } (h : i < b.to_list.length) (h' : i < b.size) :
b.to_list.nth_le i h = b.read i, h'⟩
theorem buffer.nth_le_to_list {α : Type u_1} (b : buffer α) {i : } (h : i < b.to_list.length) :
b.to_list.nth_le i h = b.read i, _⟩
theorem buffer.read_eq_nth_le_to_list {α : Type u_1} (b : buffer α) (i : fin b.size) :
theorem buffer.read_singleton {α : Type u_1} (c : α) :
[c].to_buffer.read 0, _⟩ = c
def buffer.list_equiv_buffer (α : Type u_1) :

The natural equivalence between lists and buffers, using list.to_buffer and buffer.to_list.

Equations
meta def buffer.read_t {α : Type u_1} (b : buffer α) (i : ) :

A convenience wrapper around read that just fails if the index is out of bounds.