Skip to content

Commit 1dc706d

Browse files
committed
Minor
1 parent b3e171b commit 1dc706d

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

HumanEvalLean/HumanEval67.lean

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -54,9 +54,8 @@ theorem fruitDistribution_intercalate_toString (l : List Word) (n : Nat) :
5454
fruitDistribution (" ".intercalate (l.map Word.toString)) n = n - (l.filterMap Word.toNat?).sum := by
5555
rw [fruitDistribution]
5656
simp +instances only [String.reduceToSingleton]
57-
rw [← Std.Iter.foldl_toList, Std.Iter.toList_filterMap]
58-
rw [← String.Slice.toNat?_comp_copy, ← List.filterMap_map,
59-
String.toList_split_intercalate (by simp), ← List.sum_eq_foldl]
57+
rw [← Std.Iter.foldl_toList, Std.Iter.toList_filterMap, ← String.Slice.toNat?_comp_copy,
58+
← List.filterMap_map, String.toList_split_intercalate (by simp), ← List.sum_eq_foldl]
6059
simp only [List.map_eq_nil_iff]
6160
split <;> simp_all
6261

0 commit comments

Comments
 (0)