@@ -127,6 +127,34 @@ export
127127manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
128128manyTill l end = end <|> opt (l <+> manyTill l end)
129129
130+||| Recognise a sub-lexer at least `min` times. Consumes input unless
131+||| min is zero.
132+export
133+atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
134+atLeast Z l = many l
135+atLeast (S min) l = l <+> atLeast min l
136+
137+||| Recognise a sub-lexer at most `max` times. Not guaranteed to
138+||| consume input.
139+export
140+atMost : (max : Nat) -> (l : Lexer) -> Recognise False
141+atMost Z _ = Empty
142+atMost (S k) l = atMost k l <+> opt l
143+
144+||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
145+||| if the inputs are out of order. Consumes input unless min is zero.
146+export
147+between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
148+between Z max l = atMost max l
149+between (S min) Z _ = Fail
150+between (S min) (S max) l = l <+> between min max l
151+
152+||| Recognise exactly `count` repeated occurrences of a sub-lexer.
153+||| Consumes input unless count is zero.
154+export
155+exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
156+exactly n l = between n n l
157+
130158||| Recognise any character
131159export
132160any : Lexer