module ListTest where import AlonzoPrelude import PreludeList open AlonzoPrelude open PreludeList mynil : {A:Set} -> List A mynil = [] mycons : {A:Set} -> A -> List A -> List A mycons x xs = x :: xs head : (A:Set) -> List A -> A head A (x :: xs) = x
