def pack_lift

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

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

98def pack_lift(+a: Nat, +b: Nat, coordinate: Shape.Fin(a) & Shape.Fin(b)) -> {Shape.Fin.pack(1n+a, b, Shape.Fin.unpack.lift(a, b, coordinate)) == Shape.Fin.shift(b, Nat.mul(a, b), Shape.Fin.pack(a, b, coordinate)) : Shape.Fin(Nat.add(b, Nat.mul(a, b)))}:
99  (first, last) = coordinate
100  {==}