mathlib documentation

core.data.buffer

def buffer  :
Type uType u

Equations
def mk_buffer {α : Type u} :

Equations
def array.to_buffer {α : Type u} {n : } :
array n αbuffer α

Equations
def buffer.nil {α : Type u} :

Equations
def buffer.size {α : Type u} :
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} :
buffer αlist α

Equations
def buffer.append_list {α : Type u} :
buffer αlist αbuffer α

Equations
theorem buffer.lt_aux_1 {a b c : } :
a + c < ba < b

theorem buffer.lt_aux_2 {n : } :
n > 0n - 1 < n

theorem buffer.lt_aux_3 {n i : } :
i + 1 < nn - 2 - i < n

def buffer.append_array {α : Type u} {n : } (nz : n > 0) (ᾰ : buffer α) (ᾰ_1 : array n α) (i : ) :
i < nbuffer α

Equations
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] :
buffer α(α → 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} :
buffer αbuffer α

Equations
def buffer.take_right {α : Type u} :
buffer αbuffer α

Equations
def buffer.drop {α : Type u} :
buffer αbuffer α

Equations
def buffer.reverse {α : Type u} :
buffer αbuffer α

Equations
def buffer.mem {α : Type u} :
α → buffer α → Prop

Equations
@[instance]
def buffer.has_mem {α : Type u} :
has_mem α (buffer α)

Equations
@[instance]
def buffer.has_append {α : Type u} :

Equations
@[instance]
def buffer.has_repr {α : Type u} [has_repr α] :

Equations
@[instance]
meta def buffer.has_to_format {α : Type u} [has_to_format α] :

@[instance]

def list.to_buffer {α : Type u} :
list αbuffer α

Equations
def char_buffer  :
Type

Equations
meta constant format.to_buffer  :

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