def ws

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/gcd.bend:56

import Base

56def ws(fuel: Nat, +a: Nat, +b: Nat) -> Wit:
57  match fuel b:
58    case 0n _:
59      W{1n, 0n}
60    case 1n+f 0n:
61      W{1n, 0n}
62    case 1n+f 1n+ +bp:
63      wstep(Nat.div(a, 1n+bp), ws(f, 1n+bp, Nat.mod(a, 1n+bp)))