def gw_acc

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/lists.bend:57

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as G

57# the quotient acc / gcd_all_go(xs, acc)
58def gw_acc(+xs: List<&2, Nat>, +acc: Nat) -> Nat:
59  match xs:
60    case Nil{}:
61      1n
62    case Con{+x, +t}:
63      Nat.mul(G.wl(G.ws(x, acc, x)), gw_acc(t, M.gcd(acc, x)))