mathlib documentation

core / data.buffer

def buffer (α : Type u) :
Type u

Equations
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
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 : n > 0) :
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 : n > 0) :
buffer α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] (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
def buffer.mem {α : Type u} (v : α) (a : 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} (l : list α) :

Equations
def char_buffer  :
Type

Equations
meta constant format.to_buffer  :

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