def stepped_left

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

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

243# A matmul cell steps its left offset by one word and its right offset by a
244# row of `columns` words: the term after term k sits at the offsets of k + 1.
245def stepped_left(+inner: Nat, +row: Nat, +k: Nat) ->
246  {Nat.add(1n, Nat.add(Nat.mul(row, inner), k)) == Nat.add(Nat.mul(row, inner), 1n+k) : Nat}:
247  Equal.sym(Nat, Nat.add(Nat.mul(row, inner), 1n+k), 1n+Nat.add(Nat.mul(row, inner), k), Arith.add_succ(Nat.mul(row, inner), k))