Every assignment of `program` writes a slot in [low, high).
270def dataParallelWritesWithin =
271 (lambda unrestricted slots : Nat .
272 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
273 (lambda unrestricted low : Nat .
274 (lambda unrestricted high : Nat .
275 (stdListFold
276 (family PointwiseAssignment StdU64 slots)
277 Nat
278 (lambda unrestricted assignment : (family PointwiseAssignment StdU64 slots) .
279 (lambda unrestricted rest : Nat .
280 (eliminate
281 PointwiseAssignment
282 (lambda unrestricted current : (family PointwiseAssignment StdU64 slots) . Nat)
283 assignment
284 (branch
285 PointwiseAssign
286 destination
287 expression
288 .
289 (naturalAnd
290 rest
291 (naturalAnd
292 (naturalLessOrEqual low (stdFinToNatural slots destination))
293 (naturalLess (stdFinToNatural slots destination) high)))))))
294 1
295 program)))))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.