IndexProofs.pack_unpack_step: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as IndexProofs Lines 102-108 of bendtorch-core@0.1.0.0/src/shape/index_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&start_line=102&end_line=108 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape def 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.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)))}: match split: case Inl{last}: {==} case Inr{+index}: %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)))} pack_lift(a, b, Shape.Fin.unpack(a, b, index)) Uses (12): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.merge https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.pack https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.shift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.unpack https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.unpack.lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.unpack.step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=pack_lift