The first `count` elements (all of them when the list is shorter); the
structural recursion is on the count, the list is eliminated one cell at a
time under it (Language & Testing Evolution L5: shrinkers halve lists).
221def stdListTake =
222 (lambda erased element : Type 0 .
223 (lambda unrestricted count : Nat .
224 (lambda unrestricted values : (family StdList element) .
225 (app
226 (nat-eliminate
227 (lambda unrestricted current : Nat .
228 (pi unrestricted remaining : (family StdList element) . (family StdList element)))
229 (lambda unrestricted remaining : (family StdList element) .
230 (constructor StdList StdListEmpty element))
231 (lambda unrestricted predecessor : Nat .
232 (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
233 (lambda unrestricted remaining : (family StdList element) .
234 (eliminate
235 StdList
236 (lambda unrestricted current : (family StdList element) .
237 (family StdList element))
238 remaining
239 (branch StdListEmpty . (constructor StdList StdListEmpty element))
240 (branch
241 StdListCons
242 head
243 tail
244 tailInduction
245 .
246 (constructor StdList StdListCons element head (induction tail)))))))
247 count)
248 values))))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.