author | wenzelm |
Sun, 18 Sep 2011 16:33:30 +0200 | |
changeset 44978 | a04f3eb3943c |
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 # [])"