class Buffer (σ : Type) : Type

• size : σ → ℕ

@[instance_reducible]

instance Buffer.instByteArray : Buffer ByteArray

Equations

• Buffer.instByteArray = { size := ByteArray.size }

@[simp]

theorem Buffer.size_byteArray (b : ByteArray) : size b = b.size

@[instance_reducible]

instance Buffer.instArray {τ : Type} : Buffer (Array τ)

Equations

• Buffer.instArray = { size := Array.size }

@[simp]

theorem Buffer.size_array {τ : Type} (a : Array τ) : size a = a.size