From 9301eb303c55b8f98f4d11bb072813ad90299a55 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 7 Jan 2025 11:46:49 -0500
Subject: [PATCH] Add isSubstr to Util

---
 src/Util.md | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/src/Util.md b/src/Util.md
index f015e61..3c2388e 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -6,6 +6,7 @@ This module contains functions that extend the functionality of standard data ty
 module Util
 
 import Data.SortedSet
+import Data.String
 
 %default total
 ```
@@ -66,3 +67,34 @@ Count the number of elements in a sorted set
   length : SortedSet k -> Nat
   length x = foldl (\acc, e => acc + 1) 0 x
 ```
+
+## String
+
+Extend `Data.String`
+
+<!-- idris
+namespace String
+-->
+
+### isSubstr
+
+Returns `True` if `needle` is a substring of `haystack`
+
+We first check to see if the needle is a prefix of the top level haystack, before calling into a tail recursive helper function that peels one character off of the string at a time, checking if the needle is a prefix at each step.
+
+```idris
+  export
+  isSubstr : (needle, haystack : String) -> Bool
+  isSubstr needle haystack = 
+    if needle `isPrefixOf` haystack 
+      then True
+      else isSubstr' haystack
+    where
+    isSubstr' : String -> Bool
+    isSubstr' str with (asList str)
+      isSubstr' "" | [] = False
+      isSubstr' (strCons c str) | (c :: x) = 
+        if needle `isPrefixOf` str
+          then True
+          else isSubstr' str | x
+```