66def pointwiseProgramIdentity =
67 (lambda unrestricted slots : Nat .
68 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
69 (bytes-append
70 b"alpha-pointwise-v1;"
71 (bytes-append
72 (pointwiseIdentityWord slots)
73 (bytes-append
74 (pointwiseIdentityWord
75 (stdListLength (family PointwiseAssignment StdU64 slots) program))
76 (stdListFold
77 (family PointwiseAssignment StdU64 slots)
78 Bytes
79 (lambda unrestricted assignment : (family PointwiseAssignment StdU64 slots) .
80 (lambda unrestricted rest : Bytes .
81 (eliminate
82 PointwiseAssignment
83 (lambda unrestricted current : (family PointwiseAssignment StdU64 slots) .
84 Bytes)
85 assignment
86 (branch
87 PointwiseAssign
88 destination
89 expression
90 .
91 (bytes-append
92 (pointwiseIdentityWord (stdFinToNatural slots destination))
93 (bytes-append (pointwiseExpressionIdentity slots expression) rest))))))
94 b""
95 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.