This repository was archived by the owner on Oct 7, 2020. It is now read-only.
This repository was archived by the owner on Oct 7, 2020. It is now read-only.
Features request : case split, make definition. #259
Closed
Description
I really like idris language server.
Especially the case split feature.
map2 :: (a -> b -> c) -> [a] -> [b] -> [c]
map2 f x y = undefined
Right click x and choose case split.
map2 f [] y = undefined
map2 f (x:xs) y = undefined
Now lets forget about _|_ / bottom / undefined for a moment.
What can we do with the function f
, if we don't have any variable of type a
? Nothing... lets get rid of that.
map2 _ [] _ = []
map2 f (x:xs) y = undefined
And also the named hole feature.
sum :: [Int] -> Int
-- we do not get compile error here, ?foo acts like undefined
-- you can hover over ?foo and see its type
sum = ?foo (+) 0
Right click ?foo
and select make definition.
sum :: [Int] -> Int
sum = foo (+) 0
foo :: (Int -> Int -> Int) -> Int -> [Int] -> Int
foo a b c = undefined