Skip to content

Commit 1785677

Browse files
committed
Fix
1 parent b3128f8 commit 1785677

File tree

1 file changed

+0
-3
lines changed

1 file changed

+0
-3
lines changed

HumanEvalLean/HumanEval64.lean

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,6 @@ example : vowelsCount "keY" = 2 := by native_decide
2222
example : vowelsCount "bYe" = 1 := by native_decide
2323
example : vowelsCount "ACEDY" = 3 := by native_decide
2424

25-
theorem String.back?_eq {s : String} : s.back? = s.toList.getLast? :=
26-
sorry -- https://github.com/leanprover/lean4/pull/13105
27-
2825
theorem vowelsCount_eq {s : String} :
2926
vowelsCount s = (s.toList.filter (· ∈ vowelsList)).length +
3027
(if s.toList.getLast? = some 'y' ∨ s.toList.getLast? = some 'Y' then 1 else 0) := by

0 commit comments

Comments
 (0)