MatrixIndexProof.unflatten_at: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndexProof
Lines 132-159 of bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&start_line=132&end_line=159

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as Boundary
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix

def unflatten_at(+output: Shape.Shape, +rows: Nat, +columns: Nat,
  extents: {Shape.extents(output) == [rows, columns] : List<&2, Nat>}, +position: Nat,
  +below: {Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
  {ShapeLaws.coordinate_result(output, Shape.unflatten_checked(output, U32.from_nat(position))) ==
    Some{[U32.from_nat(Matrix.row_of(columns, position)), U32.from_nat(Matrix.column_of(columns, position))]} : Maybe<&2, List<&2, U32>>}:
  +bound = Shape.numel(Shape.extents(output))
  +fits = Equal.sym(Bool, Nat.is_lt(position, bound), True{}, below)
  +index = Coordinates.fin_from(bound, position, fits)
  Equal.trans(Maybe<&2, List<&2, U32>>, ShapeLaws.coordinate_result(output, Shape.unflatten_checked(output, U32.from_nat(position))),
    ShapeLaws.unflatten_spec(Shape.extents(output), ShapeLaws.fin_of(bound, U32.to_nat(U32.from_nat(position)))),
    Some{[U32.from_nat(Matrix.row_of(columns, position)), U32.from_nat(Matrix.column_of(columns, position))]},
    Boundary.unflatten_checked(output, U32.from_nat(position)),
    Equal.trans(Maybe<&2, List<&2, U32>>,
      ShapeLaws.unflatten_spec(Shape.extents(output), ShapeLaws.fin_of(bound, U32.to_nat(U32.from_nat(position)))),
      ShapeLaws.unflatten_spec(Shape.extents(output), ShapeLaws.fin_of(bound, position)),
      Some{[U32.from_nat(Matrix.row_of(columns, position)), U32.from_nat(Matrix.column_of(columns, position))]},
      Equal.cong(Nat, Maybe<&2, List<&2, U32>>, value => ShapeLaws.unflatten_spec(Shape.extents(output), ShapeLaws.fin_of(bound, value)),
        U32.to_nat(U32.from_nat(position)), position, word_exact(position, output, below)),
      Equal.trans(Maybe<&2, List<&2, U32>>,
        ShapeLaws.unflatten_spec(Shape.extents(output), ShapeLaws.fin_of(bound, position)),
        ShapeLaws.unflatten_spec(Shape.extents(output), Some{index}),
        Some{[U32.from_nat(Matrix.row_of(columns, position)), U32.from_nat(Matrix.column_of(columns, position))]},
        Equal.cong(Maybe<&2, Shape.Fin(bound)>, Maybe<&2, List<&2, U32>>, found => ShapeLaws.unflatten_spec(Shape.extents(output), found),
          ShapeLaws.fin_of(bound, position), Some{index}, Boundary.fin_of_from(bound, position, fits)),
        Equal.cong(List<&2, Nat>, Maybe<&2, List<&2, U32>>, values => Some{Shape.words(values)},
          Shape.indices(Shape.extents(output), Shape.unflatten(Shape.extents(output), index)),
          [Matrix.row_of(columns, position), Matrix.column_of(columns, position)],
          position_digits(output, rows, columns, extents, position, fits)))))

Uses (31):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=coordinate_result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=fin_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=unflatten_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fin_of_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=unflatten_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from
  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=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  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_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=column_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=row_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=position_digits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=word_exact