@@ -113,11 +113,11 @@ export
113113many : Lexer -> Recognise False
114114many l = opt (some l)
115115
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.
117118export
118−choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
119−choice (x :: []) = x
120−choice (x :: xs@(_ :: _)) = x <|> choice xs
119+choice : Foldable t => t Lexer -> Lexer
120+choice xs = foldr Alt Fail xs
121121
122122||| Recognise many instances of `l` until an instance of `end` is
123123||| encountered.