| No other cites to report in StandardLib |
|
for_hdtl | Def ForHdTl{A,f,k} h::t as. g(h;t) == reduce(f;k;mapcons(h,t. g(h;t);as)) |
| | Thm* A,B,C:Type, f:(BCC), k:C, as:A List, g:(A(A List)B).
Thm* (ForHdTl{A,f,k} h::t as. g(h,t)) C |
|
mapcons | Def mapcons(f;as) == Case of as; nil nil ; a.as' f(a,as').mapcons(f;as')
Def (recursive) |
| | Thm* A,B:Type, f:(A(A List)B), l:A List. mapcons(f;l) B List |
|
reduce | Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as'))
Def (recursive) |
| | Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B |