x
L.P(x)) == reduce(
x,b. P(x)
b;true;L)T:Type, L:T List, P:(T
). (xL.P(x)) q == if p
q else false fip,q:. (pq) k ; a.as' f(a,reduce(f;k;as')) (recursive)A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B| Who Cites l ball? | |
| l_ball | Def (xL.P(x)) == reduce(x,b. P(x)b;true;L) |
| Thm* T:Type, L:T List, P:(T). (xL.P(x)) | |
| band | Def pq == if p q else false fi |
| Thm* p,q:. (pq) | |
| reduce | Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive) |
| Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B |
| Syntax: | (xL.P(x)) | has structure: | l_ball(L; x.P(x)) |
About:
 |  |  |
 |  |  |  |  |
 |  |  |  |  |
 |