TestQueueForceLazy.idr

%default total

interface Queue (q: Type -> Type) where   
  empty : q a 
  isEmpty : q a -> Bool
  snoc : q a -> a -> q a 
  head : q a -> a
  tail : q a -> q a 

data CatList : (Type -> Type) -> Type -> Type where
  E : CatList q a 
  C : {0 q : Type -> Type} -> a -> Lazy (q (CatList q a)) -> CatList q a 

link : Queue q => CatList q a -> Lazy (CatList q a) -> CatList q a 
link E s = s -- different to original definition.
link (C x xs) s = 
  let p1 = snoc xs s
  in C x p1