def unflatten_flatten

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

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

135def unflatten_flatten(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {Shape.unflatten(dims, Shape.flatten(dims, coordinate)) == coordinate : Shape.Coordinate(dims)}:
136  match dims:
137    case Nil{}:
138      match coordinate:
139        case Unit{}:
140          {==}
141    case +head <> +tail:
142      Shape.CStep{+first, +rest} = coordinate
143      %unflatten_flatten(tail, rest) : {Shape.unflatten(head <> tail, Shape.flatten(head <> tail, Shape.CStep{first, rest})) == Shape.CStep{first, _} : Shape.Coordinate(head <> tail)}
144      %unpack_pack(head, Shape.numel(tail), first, Shape.flatten(tail, rest)) : {Shape.unflatten.step(head, tail, last => Shape.unflatten(tail, last), Shape.Fin.unpack(head, Shape.numel(tail), Shape.Fin.pack(head, Shape.numel(tail), (first, Shape.flatten(tail, rest))))) == Shape.unflatten.step(head, tail, last => Shape.unflatten(tail, last), _) : Shape.Coordinate(head <> tail)}
145      {==}