git.iko.soy/Idris-dev
on master help sign in
Merge pull request #570 from folone/master
572db40Edwin Brady
lib/Prelude/Nat.idr+17−3
compare with master
unifiedsplit
@@ -207,9 +207,10 @@ fib Z = Z
207fib (S Z) = S Z
207fib (S Z) = S Z
208fib (S (S n)) = fib (S n) + fib n
208fib (S (S n)) = fib (S n) + fib n
209
209
210−--------------------------------------------------------------------------------
210+total fact : Nat -> Nat
211−-- GCD and LCM
211+fact Z = S Z
212−--------------------------------------------------------------------------------
212+fact (S Z) = S Z
213+fact (S n) = (S n) * fact n
213
214
214--------------------------------------------------------------------------------
215--------------------------------------------------------------------------------
215-- Division and modulus
216-- Division and modulus
@@ -245,6 +246,19 @@ log2 Z = Z
245log2 (S Z) = Z
246log2 (S Z) = Z
246log2 n = S (log2 (n `div` 2))
247log2 n = S (log2 (n `div` 2))
247
248
249+--------------------------------------------------------------------------------
250+-- GCD and LCM
251+--------------------------------------------------------------------------------
252+%assert_total
253+gcd : Nat -> Nat -> Nat
254+gcd a Z = a
255+gcd a b = gcd b (a `mod` b)
256+
257+total lcm : Nat -> Nat -> Nat
258+lcm _ Z = Z
259+lcm Z _ = Z
260+lcm x y = div (x * y) (gcd x y)
261+
248--------------------------------------------------------------------------------
262--------------------------------------------------------------------------------
249-- Properties
263-- Properties
250--------------------------------------------------------------------------------
264--------------------------------------------------------------------------------