k ; a.as' f(a,reduce(f;k;as')) (recursive)
A,B:Type, f:(A
BB), k:B, as:A List. reduce(f;k;as) 
B| Who Cites reduce? | |
| 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: | reduce(f;k;as) | has structure: | reduce(f; k; as) |
About:
 |  |  |
 |  |  |  |  |
 |