| | 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 |