1
0
Fork 0

reorder agda emit fns

This commit is contained in:
Sean Sube 2022-09-30 22:28:56 -05:00
parent ea6bbc4462
commit cb42e9cea8
1 changed files with 4 additions and 4 deletions

View File

@ -31,14 +31,14 @@ record Result (A : Set) : Set where
val : Maybe A val : Maybe A
rem : List Char rem : List Char
-- emit a result with a value and continue parsing
emit↓ : {A : Set} → A → List Char → Result A
emit↓ a rem = emit (just a) rem
-- emit a result without a value and backtrack -- emit a result without a value and backtrack
emit↑ : {A : Set} → List Char → Result A emit↑ : {A : Set} → List Char → Result A
emit↑ rem = emit nothing rem emit↑ rem = emit nothing rem
-- emit a result with a value and continue parsing
emit↓ : {A : Set} → A → List Char → Result A
emit↓ a rem = emit (just a) rem
-- take consecutive occurences of a character set -- take consecutive occurences of a character set
takeCons : List Char → List Char → Result (List Char) takeCons : List Char → List Char → Result (List Char)
takeCons _ [] = emit↑ [] takeCons _ [] = emit↑ []