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).
166def stdListTake =
167 (lambda erased element : Type 0 .
168 (lambda unrestricted count : Nat .
169 (lambda unrestricted values : (family StdList element) .
170 (app
171 (nat-eliminate
172 (lambda unrestricted current : Nat .
173 (pi unrestricted remaining : (family StdList element) . (family StdList element)))
174 (lambda unrestricted remaining : (family StdList element) .
175 (constructor StdList StdListEmpty element))
176 (lambda unrestricted predecessor : Nat .
177 (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
178 (lambda unrestricted remaining : (family StdList element) .
179 (eliminate
180 StdList
181 (lambda unrestricted current : (family StdList element) .
182 (family StdList element))
183 remaining
184 (branch StdListEmpty . (constructor StdList StdListEmpty element))
185 (branch
186 StdListCons
187 head
188 tail
189 tailInduction
190 .
191 (constructor StdList StdListCons element head (induction tail)))))))
192 count)
193 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.