| changeset 12406 | c9775847ed66 |
| parent 5184 | 9b8547a9496a |
| child 15635 | 8408a06590a6 |
| 12405:9b16f99fd7b9 | 12406:c9775847ed66 |
|---|---|
5 |
5 |
6 Simple term structure for unification. |
6 Simple term structure for unification. |
7 Binary trees with leaves that are constants or variables. |
7 Binary trees with leaves that are constants or variables. |
8 *) |
8 *) |
9 |
9 |
10 UTerm = Finite + Datatype + |
10 UTerm = Main + |
11 |
11 |
12 datatype 'a uterm = Var ('a) |
12 datatype 'a uterm = Var ('a) |
13 | Const ('a) |
13 | Const ('a) |
14 | Comb ('a uterm) ('a uterm) |
14 | Comb ('a uterm) ('a uterm) |
15 |
15 |