type Split

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

import Base

42# t = quotient * size + remainder with remainder < size.
43type Split<-t: Nat, -size: Nat> is Data:
44  Split{quotient: Nat, remainder: Nat, below: {Nat.is_lt(remainder, size) == True{} : Bool},
45    sum: {Nat.add(Nat.mul(quotient, size), remainder) == t : Nat}}