| 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 |
|
eq_int | Def i=j == if i=j true ; false fi |
| | Thm* i,j:. (i=j) |
|
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 |