
  0 | ||| Linear Bounded Queue Internals
  1 | module Data.BoundedQueue1.Unsized.Internal
  2 | 
  3 | import Data.BoundedQueue.Unsized.Internal
  4 | 
  5 | import Data.Linear.Ref1
  6 | import Derive.Prelude
  7 | 
  8 | %language ElabReflection
  9 | 
 10 | %default total
 11 | 
 12 | ||| A linear, immutable, bounded first-in first-out structure which keeps
 13 | ||| track of its size, with amortized O(1) enqueue and dequeue operations.
 14 | public export
 15 | data BoundedQueue1 : (s : Type) -> (a : Type) -> Type where
 16 |   MkBoundedQueue1 : Ref s (BoundedQueue a)
 17 |                  -> BoundedQueue1 s a
 18 |