MatrixIndexProof.flat_pair: 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 188-216 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=188&end_line=216

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

def flat_pair(+shape: Shape.Shape, +first: U32, +second: U32, +x: U32, +y: U32,
  +dimensions: {Shape.dimensions(shape) == [first, second] : List<&2, U32>},
  x_inside: {Nat.is_lt(U32.to_nat(x), U32.to_nat(first)) == True{} : Bool},
  y_inside: {Nat.is_lt(U32.to_nat(y), U32.to_nat(second)) == True{} : Bool}) ->
  {ShapeLaws.index_result(shape, Shape.flatten_checked(shape, [x, y])) ==
    Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(x), U32.to_nat(second)), U32.to_nat(y)))} : Maybe<&2, U32>}:
  +values : List<&2, Nat> = [U32.to_nat(x), U32.to_nat(y)]
  +fits = Coordinates.pair_fits(shape, first, second, x, y, dimensions, x_inside, y_inside)
  +coordinate = Coordinates.coordinate_of(Shape.extents(shape), values, fits)
  +target : Maybe<&2, U32> = Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(x), U32.to_nat(second)), U32.to_nat(y)))}
  Equal.trans(Maybe<&2, U32>, ShapeLaws.index_result(shape, Shape.flatten_checked(shape, [x, y])),
    ShapeLaws.flatten_spec(Shape.extents(shape), ShapeLaws.decode(Shape.extents(shape), values)), target,
    Boundary.flatten_checked(shape, [x, y]),
    Equal.trans(Maybe<&2, U32>, ShapeLaws.flatten_spec(Shape.extents(shape), ShapeLaws.decode(Shape.extents(shape), values)),
      Some{U32.from_nat(Shape.row_major(Shape.extents(shape), coordinate))}, target,
      Equal.cong(Maybe<&2, Shape.Coordinate(Shape.extents(shape))>, Maybe<&2, U32>, found => ShapeLaws.flatten_spec(Shape.extents(shape), found),
        ShapeLaws.decode(Shape.extents(shape), values), Some{coordinate}, Boundary.decode_fit(Shape.extents(shape), values, fits)),
      Equal.trans(Maybe<&2, U32>, Some{U32.from_nat(Shape.row_major(Shape.extents(shape), coordinate))},
        Some{U32.from_nat(Shape.offset(Shape.extents(shape), values))}, target,
        Equal.cong(Nat, Maybe<&2, U32>, offset => Some{U32.from_nat(offset)}, Shape.row_major(Shape.extents(shape), coordinate),
          Shape.offset(Shape.extents(shape), values), Coordinates.offset_of(Shape.extents(shape), values, fits)),
        Equal.trans(Maybe<&2, U32>, Some{U32.from_nat(Shape.offset(Shape.extents(shape), values))},
          Some{U32.from_nat(Shape.offset([U32.to_nat(first), U32.to_nat(second)], values))}, target,
          Equal.cong(List<&2, U32>, Maybe<&2, U32>, dims => Some{U32.from_nat(Shape.offset(Shape.naturals(dims), values))},
            Shape.dimensions(shape), [first, second], dimensions),
          Equal.cong(Nat, Maybe<&2, U32>, offset => Some{U32.from_nat(offset)},
            Shape.offset([U32.to_nat(first), U32.to_nat(second)], values),
            Nat.add(Nat.mul(U32.to_nat(x), U32.to_nat(second)), U32.to_nat(y)),
            offset_pair(U32.to_nat(x), U32.to_nat(y), U32.to_nat(first), U32.to_nat(second)))))))

Uses (29):
  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.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.add
  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=Nat.mul
  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=decode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=flatten_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=index_result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=decode_fit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=flatten_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=coordinate_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=offset_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=pair_fits
  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=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=flatten_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=row_major
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=offset_pair