def unpair_pair

bendtorch@1.3.0.0 · dtype.bend:270

import Base

270# LAW (unpair_pair): packing a list two by two and reading back as many values as it had gives the list back, in
271# order, for any length (an odd last value is paired with a 0 that the read leaves out). Proof: by induction two
272# values at a time; the pair HW{a, b} unpacks to a then b, and the rest is the induction hypothesis.
273def unpair_pair(xs: List<&2, U32>) -> {List.take(&2, U32, unpairs(pairs(xs)), List.length(&2, U32, xs)) == xs : List<&2, U32>}:
274  match xs:
275    case Nil{}:
276      {==}
277    case Con{a, Nil{}}:
278      {==}
279    case Con{+a, Con{+b, +t}}:
280      # bend-lint: disable-next bend-lint-rules/performance/unused_result -- the binder of Equal.cong's motive, used in its body not-expected-because: a law, never run
281      Equal.cong(List<&2, U32>, List<&2, U32>, l => a <> (b <> l), List.take(&2, U32, unpairs(pairs(t)), List.length(&2, U32, t)), t, unpair_pair(t))