208def pointwiseProgramWrites =
209 (lambda erased word : Type 0 .
210 (lambda erased inputs : Nat .
211 (lambda unrestricted program : (family StdList (family PointwiseAssignment word inputs)) .
212 (lambda unrestricted index : Nat .
213 (eliminate
214 StdList
215 (lambda unrestricted current : (family StdList (family PointwiseAssignment word inputs)) .
216 Nat)
217 program
218 (branch StdListEmpty . 0)
219 (branch
220 StdListCons
221 head
222 tail
223 rest
224 .
225 (eliminate
226 PointwiseAssignment
227 (lambda unrestricted current : (family PointwiseAssignment word inputs) . Nat)
228 head
229 (branch
230 PointwiseAssign
231 destination
232 expression
233 .
234 (naturalOr (naturalEqual index (stdFinToNatural inputs destination)) 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.