Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
compose_iterDef  f{i}(x) == if i=0 x else f(f{i-1}(x)) fi  (recursive)
Thm*  f:(AA), i:f{i AA
identityDef  Id(x) == x
Thm*  A:Type. Id  AA
natDef   == {i:| 0i }
Thm*    Type

About:
ifthenelseintnatural_numbersubtractsetapply
functionrecursive_def_noticeuniversememberall
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions DiscreteMath Sections DiscrMathExt Doc