176def pointwiseProgramReadsInitial =
177 (lambda erased word : Type 0 .
178 (lambda erased inputs : Nat .
179 (lambda unrestricted program : (family StdList (family PointwiseAssignment word inputs)) .
180 (lambda unrestricted index : Nat .
181 (eliminate
182 StdList
183 (lambda unrestricted current : (family StdList (family PointwiseAssignment word inputs)) .
184 Nat)
185 program
186 (branch StdListEmpty . 0)
187 (branch
188 StdListCons
189 head
190 tail
191 rest
192 .
193 (eliminate
194 PointwiseAssignment
195 (lambda unrestricted current : (family PointwiseAssignment word inputs) . Nat)
196 head
197 (branch
198 PointwiseAssign
199 destination
200 expression
201 .
202 (naturalOr
203 (pointwiseExpressionReads word inputs expression index)
204 (naturalAnd
205 (naturalIsZero (naturalEqual index (stdFinToNatural inputs destination)))
206 rest))))))))))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.