def decomposed

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

import Base

96def decomposed(+t: Nat, +size: Nat, given: Split<t, size>) -> Decomposed<t, size>:
97  Split{+q, +r, +below, +sum} = given
98  +dq = div_of(t, size, q, r, below, sum)
99  +dr = mod_of(t, size, q, r, below, sum)
100  Decomposed{
101    %Equal.sym(Nat, Nat.mod(t, size), r, dr) : {Nat.is_lt(_, size) == True{} : Bool}
102    below,
103    %Equal.sym(Nat, Nat.div(t, size), q, dq) : {Nat.add(Nat.mul(_, size), Nat.mod(t, size)) == t : Nat}
104    %Equal.sym(Nat, Nat.mod(t, size), r, dr) : {Nat.add(Nat.mul(q, size), _) == t : Nat}
105    sum}