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  
eq_intDef i=j == if i=j true ; false fi
Thm* i,j:. (i=j 
qmulDef a *q b == (a.numb.num)/(a.denb.den)
Thm* p,q:p *q q  
qdenomDef q.den == 2of(q)
Thm* q:q.den  
qnumerDef q.num == 1of(q)
Thm* q:q.num  
ratDef  == 
Thm*   Type

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

Definitions rat 1 Sections StandardLIB Doc