mathlib 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} :
buffer αbuffer α
Equations
def buffer.read {α : Type u} (b : buffer α) :
fin b.size → α
Equations
def buffer.write {α : Type u} (b : buffer α) :
fin b.sizeα → buffer α
Equations
def buffer.read' {α : Type u} [inhabited α] :
buffer α → α
Equations
def buffer.write' {α : Type u} :
buffer αα → buffer α
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} :
buffer αlist αbuffer α
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 < nbuffer α
Equations
@[protected]
def buffer.append {α : Type u} :
buffer αbuffer αbuffer α
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 wType 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]
meta def buffer.has_to_format {α : Type u} [has_to_format α] :
@[protected, instance]
def list.to_buffer {α : Type u} (l : list α) :
Equations
@[reducible]
def char_buffer  :
Type
Equations
meta constant format.to_buffer  :

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