mathlib documentation

data.buffer.basic

source
@[instance]
def buffer.inhabited {α : Type u_1} :
inhabited (buffer α)

Equations
source
@[ext]
theorem buffer.ext {α : Type u_1} {b₁ b₂ : buffer α} (a : b₁.to_list = b₂.to_list) :
b₁ = b₂

source
@[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
def buffer.list_equiv_buffer (α : Type u_1) :
list α ≃ buffer α

Equations
source
@[instance]
def buffer.traversable  :
traversable buffer

Equations
source
@[instance]
def buffer.is_lawful_traversable  :
is_lawful_traversable buffer

Equations