core: exact string

src/Parser/Interface.md

@@ -235,6 +235,20 @@ parseTheseChars cs = do
     EndOfInput => throwParseError "End of input"
 ```
 
+Attempt to parse an exact string
+
+```idris
+exactString : String -> Parser String
+exactString str with (asList str)
+  exactString "" | [] = pure ""
+  exactString input@(strCons c str) | (c :: x) = do
+    GotChar next <- parseChar (== c) id
+      | GotError err => throwParseError "Got \{show err} expected \{show c}"
+      | EndOfInput => throwParseError "End of input"
+    rest <- exactString str | x
+    pure input
+```
+
 ### Composition of boolean functions
 
 ```idris