We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent f7baee0 commit 4b54582Copy full SHA for 4b54582
src/Init/Data/String/Basic.lean
@@ -220,8 +220,8 @@ theorem String.append_empty {s : String} : s ++ "" = s := by
220
simp [← String.bytes_inj]
221
222
@[simp]
223
-theorem String.ofList_nil : String.ofList [] = "" := by
224
- simp [← String.bytes_inj]
+theorem String.ofList_nil : String.ofList [] = "" :=
+ rfl
225
226
@[deprecated String.ofList_nil (since := "2025-10-30")]
227
theorem List.asString_nil : String.ofList [] = "" :=
0 commit comments