def gcd_go
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as Naturalimport Base
49# Euclid's algorithm; b <= fuel throughout (every step lowers b).
50def gcd_go(fuel: Nat, +a: Nat, +b: Nat) -> Nat:
51 match fuel b:
52 case 0n _:
53 a
54 case 1n+f 0n:
55 a
56 case 1n+f 1n+ +bp:
57 gcd_go(f, 1n+bp, Nat.mod(a, 1n+bp))
Uses (2)
Used by (9)
- bend-collections-laws-crypto@1.0.0.0/src/math/natural:gcd
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd:gcd_both
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse:inv_r
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd:gcd_greatest
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse:inv_dvd_a
- …