equal
deleted
inserted
replaced
17 |
17 |
18 gcd :: [nat, nat] => nat |
18 gcd :: [nat, nat] => nat |
19 "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)" |
19 "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)" |
20 |
20 |
21 pow :: [nat, nat] => nat (infixl 75) |
21 pow :: [nat, nat] => nat (infixl 75) |
22 "m pow n == nat_rec n (Suc 0) (%u v.m*v)" |
22 "m pow n == nat_rec (Suc 0) (%u v.m*v) n" |
23 |
23 |
24 fac :: nat => nat |
24 fac :: nat => nat |
25 "fac m == nat_rec m (Suc 0) (%u v.(Suc u)*v)" |
25 "fac m == nat_rec (Suc 0) (%u v.(Suc u)*v) m" |
26 |
26 |
27 end |
27 end |