Nuprl - Some Definitions

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

	Some definitions of interest.

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

	Thm* p,q:. p +q q

qmul	Def a *q b == (a.numb.num)/(a.denb.den)

	Thm* p,q:. p *q q

qdenom	Def q.den == 2of(q)

	Thm* q:. q.den

qnumer	Def q.num == 1of(q)

	Thm* q:. q.num

rat	Def ==

	Thm* Type

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html