338def pointwiseProgramTemporaryValues =
339 (lambda erased word : Type 0 .
340 (lambda erased inputs : Nat .
341 (lambda unrestricted program : (family StdList (family PointwiseAssignment word inputs)) .
342 (stdListFold
343 (family PointwiseAssignment word inputs)
344 Nat
345 (lambda unrestricted assignment : (family PointwiseAssignment word inputs) .
346 (lambda unrestricted rest : Nat .
347 (eliminate
348 PointwiseAssignment
349 (lambda unrestricted current : (family PointwiseAssignment word inputs) . Nat)
350 assignment
351 (branch
352 PointwiseAssign
353 destination
354 expression
355 .
356 (let unrestricted count =
357 (pointwiseTemporaryValues word inputs expression)
358 in
359 (naturalSelect (naturalLess count rest) rest count))))))
360 0
361 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.