From 59f1eb31d0584e962098bff02cad1fc6dbe4068a Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 03:21:53 -0500
Subject: [PATCH] core: exact string

---
 src/Parser/Interface.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md
index 17c4ff9..2c65cfa 100644
--- a/src/Parser/Interface.md
+++ b/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