adamc@313: datatype list a = Nil | Cons of a * list a adamc@313: adamc@313: fun isNil (t ::: Type) (ls : list t) : bool = adamc@313: case ls of adamc@313: Nil => True adamc@313: | Cons _ => False adamc@313: adamc@313: fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t = adamc@313: case ls1 of adamc@313: Nil => ls2 adamc@313: | Cons (x, ls1') => Cons (x, append ls1' ls2) adamc@313: adamc@313: fun appendR (t ::: Type) (ls2 : list t) (ls1 : list t) : list t = adamc@313: case ls1 of adamc@313: Nil => ls2 adamc@313: | Cons (x, ls1') => Cons (x, appendR ls2 ls1') adamc@313: adamc@313: (*fun naughty (t ::: Type) (ls : list t) : list t = naughty ls*) adamc@313: adamc@313: fun append1 (t ::: Type) (ls1 : list t) (ls2 : list t) : list t = adamc@313: case ls1 of adamc@313: Nil => ls2 adamc@313: | Cons (x, ls1') => Cons (x, append2 ls2 ls1') adamc@313: adamc@313: and append2 (t ::: Type) (ls2 : list t) (ls1 : list t) : list t = adamc@313: case ls1 of adamc@313: Nil => ls2 adamc@313: | Cons (x, ls1') => Cons (x, append1 ls1' ls2)