equal
deleted
inserted
replaced
4 |
4 |
5 (* example 6 from Peter Sewell's bestiary *) |
5 (* example 6 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 (* The binding structure is too complicated, so we cannot show equivalence *) |
9 (* The binding structure is too complicated, so equivalence the |
|
10 way we define it is not true *) |
10 ML {* val _ = cheat_equivp := true *} |
11 ML {* val _ = cheat_equivp := true *} |
11 |
12 |
12 ML {* val _ = recursive := false *} |
13 ML {* val _ = recursive := false *} |
13 nominal_datatype exp6 = |
14 nominal_datatype exp6 = |
14 EVar name |
15 EVar name |