IndexProofs.unflatten_flatten: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as IndexProofs
Lines 135-145 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=135&end_line=145

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

def unflatten_flatten(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {Shape.unflatten(dims, Shape.flatten(dims, coordinate)) == coordinate : Shape.Coordinate(dims)}:
  match dims:
    case Nil{}:
      match coordinate:
        case Unit{}:
          {==}
    case +head <> +tail:
      Shape.CStep{+first, +rest} = coordinate
      %unflatten_flatten(tail, rest) : {Shape.unflatten(head <> tail, Shape.flatten(head <> tail, Shape.CStep{first, rest})) == Shape.CStep{first, _} : Shape.Coordinate(head <> tail)}
      %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)}
      {==}

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Coordinate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Coordinate.Step
  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.unpack
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=flatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten.step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=unpack_pack