Missing case in Idris.Parser
This module:
module main
using (A : Type)
data W : Type where
Ok : (r : A -> A -> Type) -> W
gave the error
src/Idris/Parser.hs:(215,23)-(223,86): Non-exhaustive patterns in case
which seemed to be repaired by this amendment for the [] case.
commit0b58ae029714f3085839998cb287dc5ecbcdce0a
authorMichael Thompson <what_is_it_to_do_anything@yahoo.com>
dateMon 11 Mar 2013, 20:05 (14 years ago)
parenta02202d
src/Idris/Parser.hs+1
@@ -213,6 +213,7 @@ openBlock = do lchar '{'
213213closeBlock :: IParser ()
214214closeBlock = do ist <- getState
215215 bs <- case brace_stack ist of
216+ [] -> eof >> return []
216217 Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
217218 Just lvl : xs -> (do i <- indent
218219 inp <- getInput