| Who Cites eq rat? |
|
eq_rat | Def a =q b == a.numb.den=b.numa.den |
| | Thm* x,y:. x =q y |
|
qdenom | Def q.den == 2of(q) |
| | Thm* q:. q.den |
|
qnumer | Def q.num == 1of(q) |
| | Thm* q:. q.num |
|
eq_int | Def i=j == if i=j true ; false fi |
| | Thm* i,j:. (i=j) |
|
pi2 | Def 2of(t) == t.2 |
| | Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p)) |
|
pi1 | Def 1of(t) == t.1 |
| | Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |