type Decomposed

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

import Base

91# t = (t / size) * size + t % size, and t % size < size.
92type Decomposed<-t: Nat, -size: Nat> is Data:
93  Decomposed{below: {Nat.is_lt(Nat.mod(t, size), size) == True{} : Bool},
94    sum: {Nat.add(Nat.mul(Nat.div(t, size), size), Nat.mod(t, size)) == t : Nat}}