| changeset 3029 | 6fd3fc3254ee |
| parent 2950 | 0911cb7bf696 |
| child 3065 | 51ef8a3cb6ef |
| child 3071 | 11f6a561eb4b |
| 3027:aa5059a00f41 | 3029:6fd3fc3254ee |
|---|---|
42 nominal_datatype ('alpha, 'beta, 'gamma) psi = |
42 nominal_datatype ('alpha, 'beta, 'gamma) psi = |
43 PsiNil |
43 PsiNil |
44 | Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" |
44 | Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" |
45 |
45 |
46 |
46 |
47 nominal_datatype 'a foo = |
|
48 Node x::"name" f::"'a foo" binds x in f |
|
49 | Leaf "'a" |
|
50 |
|
51 term "Leaf" |
|
52 |
|
53 |
|
54 |
|
55 |
|
47 end |
56 end |
48 |
57 |
49 |
58 |
50 |
59 |