| Some definitions of interest. |
|
append | Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive) |
| | Thm* T:Type, as,bs:T List. (as @ bs) T List |
|
filter | Def filter(P;l) == reduce( a,v. if P(a) [a / v] else v fi;nil;l) |
| | Thm* T:Type, P:(T![](FONT/dash.png) ![](FONT/then_med.png) ), l:T List. filter(P;l) T List |