Each literal or arithmetic node defines one temporary value. Inputs refer
to existing state. This expression traversal is representation-independent;
a target maps values to register pairs or arena words and checks its own
limit. Assignments reuse the largest expression workspace, not their sum.
321def pointwiseTemporaryValues =
322 (lambda erased word : Type 0 .
323 (lambda erased inputs : Nat .
324 (lambda unrestricted expression : (family PointwiseExpression word inputs) .
325 (pointwiseFold
326 word
327 Nat
328 inputs
329 (lambda unrestricted operation : (family PointwiseUnary) .
330 (lambda unrestricted child : Nat . (succ child)))
331 (lambda unrestricted operation : (family PointwiseBinary) .
332 (lambda unrestricted left : Nat .
333 (lambda unrestricted right : Nat . (succ (naturalAdd left right)))))
334 (lambda unrestricted bits : word . 1)
335 expression
336 (lambda unrestricted index : (family StdFin inputs) . 0)))))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.