WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites reduce?
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
:(
A
B
B
),
k
:
B
,
as
:
A
List. reduce(
f
;
k
;
as
)
B
Syntax:
reduce(
f
;
k
;
as
)
has structure:
reduce(
f
;
k
;
as
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc