159def pointwiseExpressionReads =
160 (lambda erased word : Type 0 .
161 (lambda erased inputs : Nat .
162 (lambda unrestricted expression : (family PointwiseExpression word inputs) .
163 (lambda unrestricted index : Nat .
164 (pointwiseFold
165 word
166 Nat
167 inputs
168 (lambda unrestricted operation : (family PointwiseUnary) .
169 (lambda unrestricted x : Nat . x))
170 (lambda unrestricted operation : (family PointwiseBinary) . naturalOr)
171 (lambda unrestricted bits : word . 0)
172 expression
173 (lambda unrestricted source : (family StdFin inputs) .
174 (naturalEqual index (stdFinToNatural inputs source))))))))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.