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