lmarburger · June 19, 2014 12:14
diff --git a/ltake.idr b/ltake.idr
 module lec1

 total
 ltake : Nat -> List a -> List a
 ltake Z     _         = []
 ltake _     []        = []
 ltake (S k) (x :: xs) = x :: (ltake k xs)

 -- > ltake 1 []
 -- (input):0:0:Incomplete term ltake (fromInteger 1) []
	module lec1

	total
	ltake : Nat -> List a -> List a
	ltake Z _ = []
	ltake _ [] = []
	ltake (S k) (x :: xs) = x :: (ltake k xs)

	-- > ltake 1 []
	-- (input):0:0:Incomplete term ltake (fromInteger 1) []