Definitions rat 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
assertDef b == if b True else False fi
Thm* b:b  Prop
eq_ratDef a =q b == a.numb.den=b.numa.den
Thm* x,y:x =q y  
qaddDef a +q b == (a.numb.den+b.numa.den)/(a.denb.den)
Thm* p,q:p +q q  
qmulDef a *q b == (a.numb.num)/(a.denb.den)
Thm* p,q:p *q q  
ratDef  == 
Thm*   Type

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

Definitions rat 1 Sections StandardLIB Doc