def dvd_with

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

import Base

108# d divides every element, with the quotients given: xs[i] == ks[i] d
109def dvd_with(+d: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>) -> Type:
110  match xs ks:
111    case Nil{} Nil{}:
112      Unit
113    case Nil{} Con{k, kt}:
114      Unit
115    case Con{x, t} Nil{}:
116      Empty
117    case Con{+x, +t} Con{+k, +kt}:
118      {x == Nat.mul(k, d) : Nat} & dvd_with(d, t, kt)