| Who Cites nmod? |
|
nmod | Def nmod(m;n) == if n= 0 then 0 else m rem n fi |
| | Thm* m,n: . nmod(m;n)  |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j)  |
|
bif | Def bif(b; bx.x(bx); by.y(by)) == if b x(*) else y( x.x) fi |
| | Thm* A:Type, b: , x:(b A), y:(( b) A). bif(b; bx.x(bx); by.y(by)) A |