| changeset 2480 | ac7dff1194e8 |
| parent 2454 | 9ffee4eb1ae1 |
| 2479:a9b6a00b1ba0 | 2480:ac7dff1194e8 |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 (* example 7 from Peter Sewell's bestiary *) |
5 (* example 7 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
|
9 declare [[STEPS = 31]] |
|
8 |
10 |
9 nominal_datatype exp = |
11 nominal_datatype exp = |
10 Var name |
12 Var name |
11 | Unit |
13 | Unit |
12 | Pair exp exp |
14 | Pair exp exp |