The update-program slot of owned word j of a coordinate: its parameter
(when partitioned, word 0) or optimizer-state word.
352def dpoSlotOf =
353 (lambda unrestricted k : Nat .
354 (lambda unrestricted p : Nat .
355 (lambda unrestricted word : Nat .
356 (lambda unrestricted coordinate : Nat .
357 (naturalAdd (naturalMultiply (naturalSaturatingSubtract (succ word) p) k) coordinate)))))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.