equal
deleted
inserted
replaced
37 struct |
37 struct |
38 |
38 |
39 datatype key = CombK | VarK | AtomK of string; |
39 datatype key = CombK | VarK | AtomK of string; |
40 |
40 |
41 (*Bound variables*) |
41 (*Bound variables*) |
42 fun string_of_bound i = "*B*" ^ chr i; |
42 fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256); |
43 |
43 |
44 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms. |
44 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms. |
45 Any term whose head is a Var is regarded entirely as a Var. |
45 Any term whose head is a Var is regarded entirely as a Var. |
46 Abstractions are also regarded as Vars; this covers eta-conversion |
46 Abstractions are also regarded as Vars; this covers eta-conversion |
47 and "near" eta-conversions such as %x.?P(?f(x)). |
47 and "near" eta-conversions such as %x.?P(?f(x)). |