| changeset 2440 | 0a36825b16c1 |
| parent 2438 | abafea9b39bb |
| child 2454 | 9ffee4eb1ae1 |
| 2439:cc6e281d8f72 | 2440:0a36825b16c1 |
|---|---|
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 |
8 |
9 declare [[STEPS = 15]] |
9 declare [[STEPS = 100]] |
10 |
10 |
11 nominal_datatype exp = |
11 nominal_datatype exp = |
12 EVar name |
12 EVar name |
13 | EUnit |
13 | EUnit |
14 | EPair exp exp |
14 | EPair exp exp |