From 3029432699fa8f74a11cf35a759319aa9ed2e994 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sat, 25 Jan 2025 05:07:42 -0500 Subject: [PATCH] core: export exactString --- src/Parser/Interface.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 2c65cfa..3dc4251 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -238,6 +238,7 @@ parseTheseChars cs = do Attempt to parse an exact string ```idris +export exactString : String -> Parser String exactString str with (asList str) exactString "" | [] = pure ""