Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
int_segDef  {i..j} == {k:i  k < j }
Thm*  m,n:. {m..n Type
iter_via_intsegDef  Iter(f;ui:{a..b}. e(i)
Def  == if a<b f((Iter(f;ui:{a..b-1}. e(i)),e(b-1)) else u fi
Def  (recursive)
Thm*  f:(AAA), u:Aa,b:e:({a..b}A). (Iter(f;ui:{a..b}. e(i))  A

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

Definitions IteratedBinops Sections DiscrMathExt Doc