def lw_nth

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

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/lcm.bend as LC

139def lw_nth(+xs: List<&2, Nat>, +acc: Nat, +i: Nat) -> Nat:
140  match xs i:
141    case Nil{} i0:
142      acc
143    case Con{+x, +t} 0n:
144      Nat.mul(lw_acc(t, M.lcm(acc, x)), LC.lcm_wr(acc, x))
145    case Con{+x, +t} 1n+ +j:
146      lw_nth(t, M.lcm(acc, x), j)