accumulators = A (4-register fragments from `a`) x the B fragments, slice
by slice; the first product waits on `first`, each slice after on SB2
1278def sqProducts = (lambda unrestricted accumulator : (pi unrestricted nt : Nat . Nat) . (lambda unrestricted a : Nat .
1279 (lambda unrestricted first : Nat . (lambda unrestricted tail : (family SM86Program) .
1280 (saFor 4 (lambda unrestricted k : Nat .
1281 (saFor 8 (lambda unrestricted nt : Nat .
1282 (saHmma (accumulator nt) (naturalAdd a (naturalMultiply k 4)) (saB k nt) saSB2
1283 (naturalSelect (naturalIsZero nt) (naturalSelect (naturalIsZero k) first saWait2) saWaitNone)))))
1284 tail)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.