| Some definitions of interest. |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
eq_rat | Def a =q b == a.num b.den= b.num a.den |
| | Thm* x,y: . x =q y  |
|
qadd | Def a +q b == (a.num b.den+b.num a.den)/(a.den b.den) |
| | Thm* p,q: . p +q q  |
|
rat | Def ==     |
| | Thm* Type |