def row_at

bendtorch-core@0.1.0.0 · src/tensor/matrix_index_proof.bend:99

import Base
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix

99def row_at(+row: Nat, +column: Nat, +columns: Nat, below: {Nat.is_lt(column, columns) == True{} : Bool}) ->
100  {Matrix.row_of(columns, Nat.add(Nat.mul(row, columns), column)) == row : Nat}:
101  %Equal.sym(Nat, Nat.mul(columns, 1n), columns, Nats.mul_one_right(columns)) :
102    {Nat.div(Nat.add(Nat.mul(row, columns), column), _) == row : Nat}
103  Equal.cong(Nat & Nat, Nat, pair => Pair.fst(Nat, Nat, pair), Nat.divmod(Nat.add(Nat.mul(row, columns), column), columns), (row, column),
104    Equal.sym(Nat & Nat, (row, column), Nat.divmod(Nat.add(Nat.mul(row, columns), column), columns),
105      Nats.divmod_exact(row, columns, column, lt_from(column, columns, below))))