WhoCites Definitions MarkB generic Sections NuprlLIB Doc

Who Cites reduce?
reduceDef 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:
listlist_indapply
functionrecursive_def_noticeuniversememberall
!abstraction

WhoCites Definitions MarkB generic Sections NuprlLIB Doc