Closes #12

anoma · Jan 9, 2023 · 6803647 · 6803647
1 parent ec28dc8
commit 6803647
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/Stdlib/Data/Nat/Gcd.juvix b/Stdlib/Data/Nat/Gcd.juvix
@@ -0,0 +1,14 @@
+module Stdlib.Data.Nat.Gcd;
+
+  open import Stdlib.Prelude;
+  open import Stdlib.Data.Nat.Ord;
+
+  terminating
+  gcd : Nat → Nat → Nat;
+  gcd a b :=
+    if (a == b)
+      a
+      (if (a > b)
+        (gcd (sub a b)  b)
+        (gcd a (sub b a)));
+end;