Def a +q b == (a.numb.den+b.numa.den)/(a.denb.den)

is mentioned by

Thm* a,b,c:. a *q b +q c =q a *q b +q a *q c	[qmul_dist_over_qadd]
Thm* p,q:. p +q q =q q +q p	[qadd_com]
Thm* p,q,r:. p +q q +q r =q p +q q +q r	[qadd_assoc]
Thm* p,q,r,s:. p =q q  r =q s  p +q r =q q +q s	[qadd_functionality]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html