author | clasohm |
Sat, 09 Dec 1995 13:36:11 +0100 | |
changeset 1401 | 0c439768f45c |
parent 935 | a94ef3eed456 |
child 1478 | 2b8c2a7547ab |
permissions | -rw-r--r-- |
515 | 1 |
(* Title: ZF/ex/Data.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
6 |
Sample datatype definition. |
|
7 |
It has four contructors, of arities 0-3, and two parameters A and B. |
|
8 |
*) |
|
9 |
||
935 | 10 |
Data = Datatype + |
515 | 11 |
|
12 |
consts |
|
1401 | 13 |
data :: [i,i] => i |
515 | 14 |
|
15 |
datatype |
|
16 |
"data(A,B)" = Con0 |
|
17 |
| Con1 ("a: A") |
|
18 |
| Con2 ("a: A", "b: B") |
|
19 |
| Con3 ("a: A", "b: B", "d: data(A,B)") |
|
20 |
||
21 |
end |