@@ -59,6 +59,12 @@ export
59many : Lexer -> Recognise False
59many : Lexer -> Recognise False
60many l = some l <|> Empty
60many l = some l <|> Empty
62+||| Recognize the first matching lexer from a non-empty list.
64+choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
66+choice (x :: xs@(_ :: _)) = x <|> choice xs
62||| Recognise many instances of `l` until an instance of `end` is
68||| Recognise many instances of `l` until an instance of `end` is
63||| encountered.
69||| encountered.