From 8b65f75106d1bb94a540e786999356c73fedb5af Mon Sep 17 00:00:00 2001 From: tjf801 <47402907+tjf801@users.noreply.github.com> Date: Thu, 23 May 2024 13:06:53 -0400 Subject: [PATCH] Keep `TODO`s in for future unproven string theorems Co-Authored-By: Bulhwi Cha --- Batteries/Data/String/Lemmas.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean index e7057c2386..44c9feb707 100644 --- 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