idris-0.99.2: test/regression001/reg005.idr
total map' : (a -> b) -> List a -> List b map' _ [] = [] map' f (x :: xs) = f x :: map' f xs f : a f = f
total map' : (a -> b) -> List a -> List b map' _ [] = [] map' f (x :: xs) = f x :: map' f xs f : a f = f