Agda-2.3.2.2: examples/outdated-and-incorrect/Alonzo/ListTest.agda
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