Idris2Doc : Data.Compress.Utils.FiniteBuffer

Data.Compress.Utils.FiniteBuffer

(source)

Definitions

record FiniteBuffer : Type -> Type
Totality: total
Visibility: export
Constructor: 
FB : Int -> Int -> Seq a -> FiniteBuffer a

Projections:
.buffer : FiniteBuffer a -> Seq a
.max_size : FiniteBuffer a -> Int
.size : FiniteBuffer a -> Int
empty : Nat -> FiniteBuffer a
Visibility: export
take_last : Nat -> FiniteBuffer a -> Maybe (List a)
Visibility: export
(+<) : FiniteBuffer a -> a -> FiniteBuffer a
Visibility: export
Fixity Declaration: infixr operator, level 5
(+<><) : Foldable f => FiniteBuffer a -> f a -> FiniteBuffer a
Visibility: export
Fixity Declaration: infixr operator, level 5
length : FiniteBuffer a -> Nat
Visibility: export