idris-1.3.2: test/interfaces010/interfaces010.idr

module Test

interface ListLike a where
  Elem : Type
  fromList : List Elem -> a

data Silly = None | Cons Int Silly

ListLike Silly where
  Elem = Int
  fromList [] = None
  fromList (x :: xs) = Cons x (fromList xs)