@@ -1,5 +1,7 @@
11module Text.Lexer
22
3+import Data.Bool.Extra
4+
35import public Control.Delayed
46
57%default total
@@ -61,6 +63,14 @@ export
6163reject : Recognise c -> Recognise False
6264reject = Lookahead False
6365
66+||| Sequence a list of recognisers.
67+export
68+concat : {c : Bool} -> (xs : List (Recognise c)) -> Recognise (c && isCons xs)
69+concat {c} [] = rewrite andFalseFalse c in Empty
70+concat {c} (x :: xs) = rewrite andTrueNeutral c in
71+ rewrite sym (orSameAndRightNeutral c (isCons xs)) in
72+ SeqEmpty x (concat xs)
73+
6474data StrLen : Type where
6575 MkStrLen : String -> Nat -> StrLen
6676