@@ -207,9 +207,10 @@ fib Z = Z
207207fib (S Z) = S Z
208208fib (S (S n)) = fib (S n) + fib n
209209
210−--------------------------------------------------------------------------------
211−-- GCD and LCM
212−--------------------------------------------------------------------------------
210+total fact : Nat -> Nat
211+fact Z = S Z
212+fact (S Z) = S Z
213+fact (S n) = (S n) * fact n
213214
214215--------------------------------------------------------------------------------
215216-- Division and modulus
@@ -245,6 +246,19 @@ log2 Z = Z
245246log2 (S Z) = Z
246247log2 n = S (log2 (n `div` 2))
247248
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+
248262--------------------------------------------------------------------------------
249263-- Properties
250264--------------------------------------------------------------------------------