core / data.buffer - mathlib3 docs

mathlib3 documentation

core / data.buffer

source
def mk_buffer {α : Type u} :
buffer α
Equations
source
def array.to_buffer {α : Type u} {n : ℕ} (a : array n α) :
buffer α
Equations
source
def buffer.nil {α : Type u} :
buffer α
Equations
source
def buffer.size {α : Type u} (b : buffer α) :
ℕ
Equations
source
def buffer.to_array {α : Type u} (b : buffer α) :
array b.size α
Equations
source
def buffer.push_back {α : Type u} :
buffer α → α → buffer α
Equations
source
def buffer.pop_back {α : Type u} :
buffer α → buffer α
Equations
source
def buffer.read {α : Type u} (b : buffer α) :
fin b.size → α
Equations
source
def buffer.write {α : Type u} (b : buffer α) :
fin b.size → α → buffer α
Equations
source
def buffer.read' {α : Type u} [inhabited α] :
buffer α → ℕ → α
Equations
source
def buffer.write' {α : Type u} :
buffer α → ℕ → α → buffer α
Equations
source
theorem buffer.read_eq_read' {α : Type u} [inhabited α] (b : buffer α) (i : ℕ) (h : i < b.size) :
b.read ⟨i, h⟩ = b.read' i
source
theorem buffer.write_eq_write' {α : Type u} (b : buffer α) (i : ℕ) (h : i < b.size) (v : α) :
b.write ⟨i, h⟩ v = b.write' i v
source
def buffer.to_list {α : Type u} (b : buffer α) :
list α
Equations
source
@[protected]
def buffer.to_string (b : buffer char) :
string
Equations
source
def buffer.append_list {α : Type u} :
buffer α → list α → buffer α
Equations
source
theorem buffer.lt_aux_1 {a b c : ℕ} (h : a + c < b) :
a < b
source
theorem buffer.lt_aux_2 {n : ℕ} (h : 0 < n) :
n - 1 < n
source
theorem buffer.lt_aux_3 {n i : ℕ} (h : i + 1 < n) :
n - 2 - i < n
source
def buffer.append_array {α : Type u} {n : ℕ} (nz : 0 < n) :
buffer α → array n α → Π (i : ℕ), i < n → buffer α
Equations
source
@[protected]
def buffer.append {α : Type u} :
buffer α → buffer α → buffer α
Equations
source
def buffer.iterate {α : Type u} {β : Type w} (b : buffer α) :
β → (fin b.size → α → β → β) → β
Equations
source
def buffer.foreach {α : Type u} (b : buffer α) :
(fin b.size → α → α) → buffer α
Equations
source
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
source
def buffer.map {α : Type u} {β : Type w} :
buffer α → (α → β) → buffer β

Map a function over the buffer.

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

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