@@ -113,11 +113,11 @@ export
113many : Lexer -> Recognise False
113many : Lexer -> Recognise False
114many l = opt (some l)
114many l = opt (some l)
116−||| Recognise the first matching lexer from a non-empty list.
116+||| Recognise the first matching lexer from a Foldable. Always consumes input
117+||| if one of the options succeeds. Fails if the foldable is empty.
118−choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
119+choice : Foldable t => t Lexer -> Lexer
119−choice (x :: []) = x
120+choice xs = foldr Alt Fail xs
120−choice (x :: xs@(_ :: _)) = x <|> choice xs
122||| Recognise many instances of `l` until an instance of `end` is
122||| Recognise many instances of `l` until an instance of `end` is
123||| encountered.
123||| encountered.