Dtype.unpair_pair: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/dtype.bend as Dtype
Lines 270-281 of bendtorch@1.3.0.0/dtype.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/dtype.bend&start_line=270&end_line=281

import Base

# LAW (unpair_pair): packing a list two by two and reading back as many values as it had gives the list back, in
# order, for any length (an odd last value is paired with a 0 that the read leaves out). Proof: by induction two
# values at a time; the pair HW{a, b} unpacks to a then b, and the rest is the induction hypothesis.
def unpair_pair(xs: List<&2, U32>) -> {List.take(&2, U32, unpairs(pairs(xs)), List.length(&2, U32, xs)) == xs : List<&2, U32>}:
  match xs:
    case Nil{}:
      {==}
    case Con{a, Nil{}}:
      {==}
    case Con{+a, Con{+b, +t}}:
      # 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
      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))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/dtype.bend&name=pairs
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/dtype.bend&name=unpairs