equal
deleted
inserted
replaced
4 Basic functions for nominal. |
4 Basic functions for nominal. |
5 *) |
5 *) |
6 |
6 |
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
|
9 val last2: 'a list -> 'a * 'a |
|
10 |
9 val dest_listT: typ -> typ |
11 val dest_listT: typ -> typ |
10 |
12 |
11 val mk_minus: term -> term |
13 val mk_minus: term -> term |
12 val mk_plus: term -> term -> term |
14 val mk_plus: term -> term -> term |
13 |
15 |
55 |
57 |
56 |
58 |
57 structure Nominal_Library: NOMINAL_LIBRARY = |
59 structure Nominal_Library: NOMINAL_LIBRARY = |
58 struct |
60 struct |
59 |
61 |
60 (* this function should be in hologic.ML *) |
62 fun last2 [] = raise Empty |
|
63 | last2 [_] = raise Empty |
|
64 | last2 [x, y] = (x,y) |
|
65 | last2 (_ :: xs) = last2 xs |
|
66 |
61 fun dest_listT (Type (@{type_name list}, [T])) = T |
67 fun dest_listT (Type (@{type_name list}, [T])) = T |
62 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
68 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
63 |
69 |
64 fun mk_minus p = @{term "uminus::perm => perm"} $ p; |
70 fun mk_minus p = @{term "uminus::perm => perm"} $ p; |
65 |
71 |