def gw_nth

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

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

72# the quotient (xs[i]) / gcd_all_go(xs, acc)
73def gw_nth(+xs: List<&2, Nat>, +acc: Nat, +i: Nat) -> Nat:
74  match xs i:
75    case Nil{} i0:
76      0n
77    case Con{+x, +t} 0n:
78      Nat.mul(G.wr(G.ws(x, acc, x)), gw_acc(t, M.gcd(acc, x)))
79    case Con{+x, +t} 1n+ +j:
80      gw_nth(t, M.gcd(acc, x), j)