Definitions FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
eval_factorizationDef  {a..b}(f) ==  i:{a..b}. if(i)
Thm*  a,b:f:({a..b}). {a..b}(f 
int_segDef  {i..j} == {k:i  k < j }
Thm*  m,n:. {m..n Type
prime_natsDef  Prime == {x:| prime(x) }
natDef   == {i:| 0i }
Thm*    Type
prime_mset_completeDef  prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi
Thm*  f:(Prime). prime_mset_complete(f 

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

Definitions FTA Sections DiscrMathExt Doc