Lists.lw_nth: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend as Lists
Lines 139-146 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend&start_line=139&end_line=146

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

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

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=lcm_wr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend&name=lw_acc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=lcm