@@ -48,6 +48,12 @@ export
4848isNot : Char -> Lexer
4949isNot x = Pred (/=x)
5050
51+||| Recognise a lexer or recognise no input. This is not guaranteed
52+||| to consume input
53+export
54+opt : Lexer -> Recognise False
55+opt l = l <|> Empty
56+
5157||| Recognise a sequence of at least one sub-lexers
5258export
5359some : Lexer -> Lexer
@@ -59,7 +65,7 @@ export
5965many : Lexer -> Recognise False
6066many l = some l <|> Empty
6167
62−||| Recognize the first matching lexer from a non-empty list.
68+||| Recognise the first matching lexer from a non-empty list.
6369export
6470choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
6571choice (x :: []) = x