95def nativePointwiseSupported =
96 (lambda unrestricted slots : Nat .
97 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
98 (stdListFold
99 (family PointwiseAssignment StdU64 slots)
100 Nat
101 (lambda unrestricted assignment : (family PointwiseAssignment StdU64 slots) .
102 (lambda unrestricted rest : Nat .
103 (eliminate
104 PointwiseAssignment
105 (lambda unrestricted current : (family PointwiseAssignment StdU64 slots) . Nat)
106 assignment
107 (branch
108 PointwiseAssign
109 destination
110 expression
111 .
112 (naturalAnd
113 rest
114 (pointwiseFold
115 StdU64
116 Nat
117 slots
118 (lambda unrestricted operation : (family PointwiseUnary) .
119 (lambda unrestricted child : Nat .
120 (naturalAnd (nativePointwiseUnarySupported operation) child)))
121 (lambda unrestricted operation : (family PointwiseBinary) .
122 (lambda unrestricted left : Nat .
123 (lambda unrestricted right : Nat .
124 (naturalAnd
125 (nativePointwiseBinarySupported operation)
126 (naturalAnd left right)))))
127 (lambda unrestricted word : StdU64 . 1)
128 expression
129 (lambda unrestricted index : (family StdFin slots) . 1)))))))
130 1
131 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.