author | wenzelm |
Tue, 03 May 2011 20:58:42 +0200 | |
changeset 42660 | e40648514b34 |
parent 38430 | 254a021ed66e |
permissions | -rw-r--r-- |
theory ToyList imports Datatype begin datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) (* This is the append function: *) primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) where "[] @ ys = ys" | "(x # xs) @ ys = x # (xs @ ys)" primrec rev :: "'a list => 'a list" where "rev [] = []" | "rev (x # xs) = (rev xs) @ (x # [])"