| changeset 2438 | abafea9b39bb |
| parent 2436 | 3885dc2669f9 |
| child 2440 | 0a36825b16c1 |
| 2436:3885dc2669f9 | 2438:abafea9b39bb |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 (* example 8 from Peter Sewell's bestiary *) |
5 (* example 8 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
|
9 declare [[STEPS = 15]] |
|
8 |
10 |
9 nominal_datatype exp = |
11 nominal_datatype exp = |
10 EVar name |
12 EVar name |
11 | EUnit |
13 | EUnit |
12 | EPair exp exp |
14 | EPair exp exp |