@[instance]
Equations
- buffer.inhabited = {default := buffer.nil α}
@[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 (λ (a : fst = w_fst), eq.rec (λ (w_snd : array fst α), decidable.by_cases (λ (a : snd = w_snd), eq.rec (decidable.is_true _) a) (λ (a : ¬snd = w_snd), decidable.is_false _)) a w_snd) (λ (a : ¬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
Equations
- buffer.list_equiv_buffer α = {to_fun := list.to_buffer α, inv_fun := buffer.to_list α, left_inv := _, right_inv := _}
@[instance]