Idris/advent
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

core: export exactString

Browse source
This commit is contained in:
Nathan McCarty 2025-01-25 05:07:42 -05:00
parent 59f1eb31d0
commit 3029432699
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Parser/Interface.md
View file

@ -238,6 +238,7 @@ parseTheseChars cs = do
Attempt to parse an exact string Attempt to parse an exact string
```idris ```idris
export
exactString : String -> Parser String exactString : String -> Parser String
exactString str with (asList str) exactString str with (asList str)
exactString "" | [] = pure "" exactString "" | [] = pure ""