def split_divmod

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:75

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/matrix_index_proof.bend as MatrixIndex

75# The quotient and remainder of a split are Nat.div and Nat.mod.
76def split_divmod(-t: Nat, +size: Nat, +q: Nat, +r: Nat, below: {Nat.is_lt(r, size) == True{} : Bool},
77  sum: {Nat.add(Nat.mul(q, size), r) == t : Nat}) -> {(q, r) == Nat.divmod(t, size) : Nat & Nat}:
78  %sum : {(q, r) == Nat.divmod(_, size) : Nat & Nat}
79  Nats.divmod_exact(q, size, r, MatrixIndex.lt_from(r, size, below))