@[protected, instance]
Equations
- buffer.inhabited = {default := buffer.nil α}
@[protected, instance]
Equations
- buffer.decidable_eq α = id (λ (_v : buffer α), sigma.cases_on _v (λ (fst : ℕ) (snd : array fst α) (w : buffer α), sigma.cases_on w (λ (w_fst : ℕ) (w_snd : array w_fst α), decidable.by_cases (λ (ᾰ : fst = w_fst), eq.rec (λ (w_snd : array fst α), decidable.by_cases (λ (ᾰ : snd = w_snd), eq.rec (decidable.is_true _) ᾰ) (λ (ᾰ : ¬snd = w_snd), decidable.is_false _)) ᾰ w_snd) (λ (ᾰ : ¬fst = w_fst), decidable.is_false _))))
@[simp]
theorem
buffer.to_list_append_list
{α : Type u_1}
{xs : list α}
{b : buffer α} :
(b.append_list xs).to_list = b.to_list ++ xs
@[simp]
theorem
buffer.append_list_mk_buffer
{α : Type u_1}
{xs : list α} :
mk_buffer.append_list xs = xs.to_array.to_buffer
@[simp]
theorem
buffer.to_buffer_cons
{α : Type u_1}
(c : α)
(l : list α) :
(c :: l).to_buffer = [c].to_buffer.append_list l
@[simp]
The natural equivalence between lists and buffers, using
list.to_buffer
and buffer.to_list
.
Equations
- buffer.list_equiv_buffer α = {to_fun := list.to_buffer α, inv_fun := buffer.to_list α, left_inv := _, right_inv := _}
@[protected, instance]
@[protected, instance]