f:(T
AT), P:(A
), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y)
f(i,y) else i fi;s;L)P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1)
a,v. if P(a) [a / v] else v fi;nil;l)
is mentioned by
| Thm* f:(TAT), P:(A), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y) f(i,y) else i fi;s;L) | [list_accum_filter] |
| Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1) | [filter_list_accum] |
In prior sections: mb list 1 mb list 2
Try larger context:
Graphs