def mul_with

bend-collections-laws-math@1.0.0.0 · spec/math/natural.bend:120

import Base

120# m is a multiple of every element, with the quotients given: m == ks[i] xs[i]
121def mul_with(+m: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>) -> Type:
122  match xs ks:
123    case Nil{} Nil{}:
124      Unit
125    case Nil{} Con{k, kt}:
126      Unit
127    case Con{x, t} Nil{}:
128      Empty
129    case Con{+x, +t} Con{+k, +kt}:
130      {m == Nat.mul(k, x) : Nat} & mul_with(m, t, kt)