blob: 58c821094e0ab23908508c0d6ffc31e3d7bc5b82 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
|
namespace Euclid
-- Extended Euclidean algorithm, stolen from Wikipedia.
-- The signature is stolen from Wikipedia too. As in, the values a and b are Nat, but s and t are Int.
def xgcd (a b: Nat) : Nat × Int × Int :=
if p : b > 0 then
have : a % b < b := by simp[p, Nat.mod_lt]
let (d, ss, tt) := xgcd b (a%b)
(d, tt ,ss - tt * (a / b))
else
(a,1,0)
termination_by xgcd a b => b
|
