equal
deleted
inserted
replaced
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 val partitions: 'a list -> int list -> 'a list list |
|
13 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
13 |
14 |
14 val is_true: term -> bool |
15 val is_true: term -> bool |
15 |
16 |
16 val dest_listT: typ -> typ |
17 val dest_listT: typ -> typ |
17 val dest_fsetT: typ -> typ |
18 val dest_fsetT: typ -> typ |
144 val (head, tail) = chop i xs |
145 val (head, tail) = chop i xs |
145 in |
146 in |
146 head :: partitions tail js |
147 head :: partitions tail js |
147 end |
148 end |
148 |
149 |
|
150 fun split_filter f [] = ([], []) |
|
151 | split_filter f (x :: xs) = |
|
152 let |
|
153 val (r, l) = split_filter f xs |
|
154 in |
|
155 if f x |
|
156 then (x :: r, l) |
|
157 else (r, x :: l) |
|
158 end |
149 |
159 |
150 |
160 |
151 fun is_true @{term "Trueprop True"} = true |
161 fun is_true @{term "Trueprop True"} = true |
152 | is_true _ = false |
162 | is_true _ = false |
153 |
163 |