mathlib documentation

data.buffer.basic

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

Equations
@[ext]
theorem buffer.ext {α : Type u_1} {b₁ b₂ : buffer α} :
b₁.to_list = b₂.to_listb₁ = b₂

@[instance]
def buffer.decidable_eq (α : Type u_1) [decidable_eq α] :

Equations
@[simp]
theorem buffer.to_list_append_list {α : Type u_1} {xs : list α} {b : buffer α} :

@[simp]
theorem buffer.append_list_mk_buffer {α : Type u_1} {xs : list α} :

def buffer.list_equiv_buffer (α : Type u_1) :

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

Equations