summaryrefslogtreecommitdiff
path: root/Common
diff options
context:
space:
mode:
Diffstat (limited to 'Common')
-rw-r--r--Common/Substring.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/Common/Substring.lean b/Common/Substring.lean
index 4ed39b4..f51b088 100644
--- a/Common/Substring.lean
+++ b/Common/Substring.lean
@@ -5,7 +5,7 @@ namespace Substring
theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos) : s.nextn n p ≥ p := by
unfold Substring.nextn
cases n
- case zero => simp[String.Pos.le_iff]
+ case zero => simp
case succ nn =>
simp
unfold Substring.next