mathlib3 documentation

core / data.buffer

def mk_buffer {α : Type u} :
Equations
def array.to_buffer {α : Type u} {n : } (a : array n α) :
Equations
def buffer.nil {α : Type u} :
Equations
def buffer.size {α : Type u} (b : buffer α) :
Equations
def buffer.to_array {α : Type u} (b : buffer α) :
array b.size α
Equations
def buffer.push_back {α : Type u} :
buffer α α buffer α
Equations
def buffer.pop_back {α : Type u} :
Equations
def buffer.read {α : Type u} (b : buffer α) :
fin b.size α
Equations
def buffer.write {α : Type u} (b : buffer α) :
Equations
def buffer.read' {α : Type u} [inhabited α] :
Equations
def buffer.write' {α : Type u} :
Equations
theorem buffer.read_eq_read' {α : Type u} [inhabited α] (b : buffer α) (i : ) (h : i < b.size) :
b.read i, h⟩ = b.read' i
theorem buffer.write_eq_write' {α : Type u} (b : buffer α) (i : ) (h : i < b.size) (v : α) :
b.write i, h⟩ v = b.write' i v
def buffer.to_list {α : Type u} (b : buffer α) :
list α
Equations
@[protected]
Equations
def buffer.append_list {α : Type u} :
Equations
theorem buffer.lt_aux_1 {a b c : } (h : a + c < b) :
a < b
theorem buffer.lt_aux_2 {n : } (h : 0 < n) :
n - 1 < n
theorem buffer.lt_aux_3 {n i : } (h : i + 1 < n) :
n - 2 - i < n
def buffer.append_array {α : Type u} {n : } (nz : 0 < n) :
buffer α array n α Π (i : ), i < n buffer α
Equations
@[protected]
def buffer.append {α : Type u} :
Equations
def buffer.iterate {α : Type u} {β : Type w} (b : buffer α) :
β (fin b.size α β β) β
Equations
def buffer.foreach {α : Type u} (b : buffer α) :
(fin b.size α α) buffer α
Equations
def buffer.mmap {α : Type u} {β : Type w} {m : Type w Type u_1} [monad m] (b : buffer α) (f : α m β) :
m (buffer β)

Monadically map a function over the buffer.

Equations
def buffer.map {α : Type u} {β : Type w} :
buffer α β) buffer β

Map a function over the buffer.

Equations
def buffer.foldl {α : Type u} {β : Type w} :
buffer α β β β) β
Equations
def buffer.rev_iterate {α : Type u} {β : Type w} (b : buffer α) :
β (fin b.size α β β) β
Equations
def buffer.take {α : Type u} (b : buffer α) (n : ) :
Equations
def buffer.take_right {α : Type u} (b : buffer α) (n : ) :
Equations
def buffer.drop {α : Type u} (b : buffer α) (n : ) :
Equations
def buffer.reverse {α : Type u} (b : buffer α) :
Equations
@[protected]
def buffer.mem {α : Type u} (v : α) (a : buffer α) :
Prop
Equations
@[protected, instance]
def buffer.has_mem {α : Type u} :
has_mem α (buffer α)
Equations
@[protected, instance]
def buffer.has_append {α : Type u} :
Equations
@[protected, instance]
def buffer.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
@[protected, instance]
def list.to_buffer {α : Type u} (l : list α) :
Equations
@[reducible]
def char_buffer  :
Equations

Convert a format object into a character buffer with the provided formatting options.