| Some definitions of interest. |
|
assert | Def b == if b True else False fi |
| | Thm* b:. b Prop |
|
eq_rat | Def a =q b == a.numb.den=b.numa.den |
| | Thm* x,y:. x =q y |
|
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 |
|
rat | Def == |
| | Thm* Type |