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