@@ -54,9 +54,9 @@ failure : String -> Parser a
5454failure msg = P (\inp => Left msg)
5555
5656item : Parser Char
57−item = P (\inp => case unpack inp of
58− [] => Left "Error! Parsing empty list."
59− (x::xs) => Right (x, pack xs))
57+item = P (\inp => case choose (inp == "") of
58+ Left _ => Left "Error! Parsing empty list."
59+ Right p => Right (strHead' inp p, strTail' inp p))
6060
6161
6262--------------------------------------------------------------------------------
@@ -92,12 +92,12 @@ char x = sat (== x)
9292string : String -> Parser String
9393string s = map pack (traverse char (unpack s))
9494
95−many1 : Parser a -> Parser (List a)
96−many : Parser a -> Parser (List a)
95+mutual
96+ many1 : Parser a -> Parser (List a)
97+ many1 p = [| p :: many p |]
9798
98−many1 p = [| p :: many p |]
99−
100−many p = lazy (many1 p) <|> pure []
99+ many : Parser a -> Parser (List a)
100+ many p = lazy (many1 p) <|> pure []
101101
102102bool : Parser Bool
103103bool = parseTrue <|> parseFalse