def flatten_unflatten_step

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

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

118def flatten_unflatten_step(+head: Nat, +tail: List<&2, Nat>, rec: @+index: Shape.Fin(Shape.numel(tail)) -> {Shape.flatten(tail, Shape.unflatten(tail, index)) == index : Shape.Fin(Shape.numel(tail))}, coordinate: Shape.Fin(head) & Shape.Fin(Shape.numel(tail))) -> {Shape.flatten(head <> tail, Shape.unflatten.step(head, tail, rest => Shape.unflatten(tail, rest), coordinate)) == Shape.Fin.pack(head, Shape.numel(tail), coordinate) : Shape.Fin(Shape.numel(head <> tail))}:
119  (first, +last) = coordinate
120  %rec(last) : {Shape.Fin.pack(head, Shape.numel(tail), (first, Shape.flatten(tail, Shape.unflatten(tail, last)))) == Shape.Fin.pack(head, Shape.numel(tail), (first, _)) : Shape.Fin(Shape.numel(head <> tail))}
121  {==}