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