equal
deleted
inserted
replaced
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
9 val last2: 'a list -> 'a * 'a |
9 val last2: 'a list -> 'a * 'a |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
11 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
11 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
|
12 val partitions: 'a list -> int list -> 'a list list |
12 |
13 |
13 val is_true: term -> bool |
14 val is_true: term -> bool |
14 |
15 |
15 val dest_listT: typ -> typ |
16 val dest_listT: typ -> typ |
16 val dest_fsetT: typ -> typ |
17 val dest_fsetT: typ -> typ |
133 |
134 |
134 fun last2 [] = raise Empty |
135 fun last2 [] = raise Empty |
135 | last2 [_] = raise Empty |
136 | last2 [_] = raise Empty |
136 | last2 [x, y] = (x, y) |
137 | last2 [x, y] = (x, y) |
137 | last2 (_ :: xs) = last2 xs |
138 | last2 (_ :: xs) = last2 xs |
|
139 |
|
140 (* partitions a set according to the numbers in the int list *) |
|
141 fun partitions [] [] = [] |
|
142 | partitions xs (i :: js) = |
|
143 let |
|
144 val (head, tail) = chop i xs |
|
145 in |
|
146 head :: partitions tail js |
|
147 end |
|
148 |
|
149 |
138 |
150 |
139 fun is_true @{term "Trueprop True"} = true |
151 fun is_true @{term "Trueprop True"} = true |
140 | is_true _ = false |
152 | is_true _ = false |
141 |
153 |
142 fun dest_listT (Type (@{type_name list}, [T])) = T |
154 fun dest_listT (Type (@{type_name list}, [T])) = T |