Everything after the first `count` elements.
196def stdListDrop =
197 (lambda erased element : Type 0 .
198 (lambda unrestricted count : Nat .
199 (lambda unrestricted values : (family StdList element) .
200 (app
201 (nat-eliminate
202 (lambda unrestricted current : Nat .
203 (pi unrestricted remaining : (family StdList element) . (family StdList element)))
204 (lambda unrestricted remaining : (family StdList element) . remaining)
205 (lambda unrestricted predecessor : Nat .
206 (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
207 (lambda unrestricted remaining : (family StdList element) .
208 (eliminate
209 StdList
210 (lambda unrestricted current : (family StdList element) .
211 (family StdList element))
212 remaining
213 (branch StdListEmpty . (constructor StdList StdListEmpty element))
214 (branch StdListCons head tail tailInduction . (induction tail))))))
215 count)
216 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.