doc-src/Tutorial/ToyList/ToyList.thy
author berghofe
Thu, 23 Sep 2004 10:20:52 +0200
changeset 15204 d15f85347fcb
parent 5377 efb799c5ed3c
permissions -rw-r--r--
- Inserted additional check for equality types in check_mode_clause that avoids ill-typed code to be generated. - Mode inference algorithm now outputs additional diagnostic messages.

ToyList = Datatype +

datatype 'a list = Nil                        ("[]")
                 | Cons 'a ('a list)          (infixr "#" 65)

consts app :: 'a list => 'a list => 'a list   (infixr "@" 65)
       rev :: 'a list => 'a list

primrec
"[] @ ys       = ys"
"(x # xs) @ ys = x # (xs @ ys)"

primrec
"rev []        = []"
"rev (x # xs)  = (rev xs) @ (x # [])"

end