Combine two lists position by position, keeping their order; the result is
as long as the SHORTER list (the rest of the longer one is dropped -- callers
that need equal lengths must establish them). The left list is eliminated
into a function of the right one, so both spines are walked together.
192def stdListZipWith =
193 (lambda erased left : Type 0 .
194 (lambda erased right : Type 0 .
195 (lambda erased result : Type 0 .
196 (lambda unrestricted combine : (pi unrestricted l : left . (pi unrestricted r : right . result)) .
197 (lambda unrestricted lefts : (family StdList left) .
198 (lambda unrestricted rights : (family StdList right) .
199 (app
200 (eliminate
201 StdList
202 (lambda unrestricted current : (family StdList left) .
203 (pi unrestricted others : (family StdList right) . (family StdList result)))
204 lefts
205 (branch StdListEmpty .
206 (lambda unrestricted others : (family StdList right) . (constructor StdList StdListEmpty result)))
207 (branch StdListCons head tail induction .
208 (lambda unrestricted others : (family StdList right) .
209 (eliminate
210 StdList
211 (lambda unrestricted inner : (family StdList right) . (family StdList result))
212 others
213 (branch StdListEmpty . (constructor StdList StdListEmpty result))
214 (branch StdListCons otherHead otherTail otherInduction .
215 (constructor StdList StdListCons result (combine head otherHead) (induction otherTail)))))))
216 rights)))))))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.