Entry	Value
Package Name	list-take-drop-def
Count	4
Theorems	drop_suc : !n h t. n <= LENGTH t ==> drop (SUC n) (CONS h t) = drop n t drop_zero : !l. drop 0 l = l take_suc : !n h t. n <= LENGTH t ==> take (SUC n) (CONS h t) = CONS h (take n t) take_zero : !l. take 0 l = []

Back to main package page