mathlib3 documentation

data.buffer.basic

source
@[protected, instance]
def buffer.inhabited {α : Type u_1} :
inhabited (buffer α)
Equations
source
@[ext]
theorem buffer.ext {α : Type u_1} {b₁ b₂ : buffer α} :
b₁.to_list = b₂.to_list → b₁ = b₂
source
theorem buffer.ext_iff {α : Type u_1} {b₁ b₂ : buffer α} :
b₁ = b₂ ↔ b₁.to_list = b₂.to_list
source
theorem buffer.size_eq_zero_iff {α : Type u_1} {b : buffer α} :
b.size = 0 ↔ b = buffer.nil
source
@[simp]
theorem buffer.size_nil {α : Type u_1} :
buffer.nil.size = 0
source
@[simp]
theorem buffer.to_list_nil {α : Type u_1} :
buffer.nil.to_list = list.nil
source
@[protected, instance]
def buffer.decidable_eq (α : Type u_1) [decidable_eq α] :
decidable_eq (buffer α)
Equations
source
@[simp]
theorem buffer.to_list_append_list {α : Type u_1} {xs : list α} {b : buffer α} :
(b.append_list xs).to_list = b.to_list ++ xs
source
@[simp]
theorem buffer.append_list_mk_buffer {α : Type u_1} {xs : list α} :
mk_buffer.append_list xs = xs.to_array.to_buffer
source
@[simp]
theorem buffer.to_buffer_to_list {α : Type u_1} (b : buffer α) :
b.to_list.to_buffer = b
source
@[simp]
theorem buffer.to_list_to_buffer {α : Type u_1} (l : list α) :
l.to_buffer.to_list = l
source
@[simp]
theorem buffer.to_list_to_array {α : Type u_1} (b : buffer α) :
b.to_array.to_list = b.to_list
source
@[simp]
theorem buffer.append_list_nil {α : Type u_1} (b : buffer α) :
b.append_list list.nil = b
source
theorem buffer.to_buffer_cons {α : Type u_1} (c : α) (l : list α) :
(c :: l).to_buffer = [c].to_buffer.append_list l
source
@[simp]
theorem buffer.size_push_back {α : Type u_1} (b : buffer α) (a : α) :
(b.push_back a).size = b.size + 1
source
@[simp]
theorem buffer.size_append_list {α : Type u_1} (b : buffer α) (l : list α) :
(b.append_list l).size = b.size + l.length
source
@[simp]
theorem buffer.size_to_buffer {α : Type u_1} (l : list α) :
l.to_buffer.size = l.length
source
@[simp]
theorem buffer.length_to_list {α : Type u_1} (b : buffer α) :
b.to_list.length = b.size
source
theorem buffer.size_singleton {α : Type u_1} (a : α) :
[a].to_buffer.size = 1
source
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⟩
source
@[simp]
theorem buffer.read_push_back_right {α : Type u_1} (b : buffer α) (a : α) :
(b.push_back a).read ⟨b.size, _⟩ = a
source
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'⟩
source
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⟩
source
@[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
source
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'
source
@[simp]
theorem buffer.read_to_buffer {α : Type u_1} (l : list α) (i : fin l.to_buffer.size) :
l.to_buffer.read i = l.nth_le ↑i _
source
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'⟩
source
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, _⟩
source
theorem buffer.read_eq_nth_le_to_list {α : Type u_1} (b : buffer α) (i : fin b.size) :
b.read i = b.to_list.nth_le ↑i _
source
theorem buffer.read_singleton {α : Type u_1} (c : α) :
[c].to_buffer.read ⟨0, _⟩ = c
source
def buffer.list_equiv_buffer (α : Type u_1) :
list α ≃ buffer α

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

Equations
source
@[protected, instance]
def buffer.traversable  :
traversable buffer
Equations
source
@[protected, instance]
def buffer.is_lawful_traversable  :
is_lawful_traversable buffer
Equations
source
meta def buffer.read_t {α : Type u_1} (b : buffer α) (i : ℕ) :
tactic α

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