
  0 | module Deque
  1 | 
  2 | %default total
  3 | 
  4 | public export
  5 | interface Deque (q : Type -> Type) where
  6 |   empty : q a
  7 |   isEmpty : q a -> Bool
  8 | 
  9 |   cons : a -> q a -> q a
 10 |   head : q a -> a
 11 |   tail : q a -> q a
 12 | 
 13 |   snoc : q a -> a -> q a
 14 |   last : q a -> a
 15 |   init : q a -> q a
 16 |