Keep TODOs in for future unproven string theorems

Co-Authored-By: Bulhwi Cha <[email protected]>
leanprover-community · May 23, 2024 · 8b65f75 · 8b65f75
1 parent 2aabdc1
commit 8b65f75
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
@@ -990,6 +990,8 @@ theorem data_isPrefixOf_iff_isPrefixOf {s t : String} : s.1.isPrefixOf t.1 ↔ s
       exact (isPrefixOf_cons.mp h).imp_right data_isPrefixOf_iff_isPrefixOf.mpr
 termination_by s.length
 
+-- TODO: substrEq
+-- TODO: isPrefixOf
 -- TODO: replace
 
 @[nolint unusedHavesSuffices] -- false positive from unfolding String.takeWhileAux