def pack_unpack_step

bendtorch-core@0.1.0.0 · src/shape/index_proofs.bend:102

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

102def pack_unpack_step(+a: Nat, +b: Nat, rec: @+index: Shape.Fin(Nat.mul(a, b)) -> {Shape.Fin.pack(a, b, Shape.Fin.unpack(a, b, index)) == index : Shape.Fin(Nat.mul(a, b))}, split: Either<Shape.Fin(b), Shape.Fin(Nat.mul(a, b))>) -> {Shape.Fin.pack(1n+a, b, Shape.Fin.unpack.step(a, b, index => Shape.Fin.unpack(a, b, index), split)) == Shape.Fin.merge(b, Nat.mul(a, b), split) : Shape.Fin(Nat.add(b, Nat.mul(a, b)))}:
103  match split:
104    case Inl{last}:
105      {==}
106    case Inr{+index}:
107      %rec(index) : {Shape.Fin.pack(1n+a, b, Shape.Fin.unpack.lift(a, b, Shape.Fin.unpack(a, b, index))) == Shape.Fin.shift(b, Nat.mul(a, b), _) : Shape.Fin(Nat.add(b, Nat.mul(a, b)))}
108      pack_lift(a, b, Shape.Fin.unpack(a, b, index))