We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent db75b31 commit 3e60c00Copy full SHA for 3e60c00
HumanEvalLean/HumanEval28.lean
@@ -5,7 +5,6 @@ def concatenate (strings : List String) : String :=
5
6
theorem toList_concatenate {strings : List String} :
7
(concatenate strings).toList = strings.flatMap String.toList := by
8
- -- https://github.com/leanprover/lean4/pull/13091
9
simp [concatenate]
10
11
/-!
0 commit comments