We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
2 parents 6216b99 + a1b4b26 commit 3b0c2c6Copy full SHA for 3b0c2c6
Batteries/Data/String/Lemmas.lean
@@ -22,6 +22,8 @@ import all Init.Data.String.Legacy -- for unfolding `String.splitOnAux`
22
23
@[expose] public section
24
25
+set_option linter.deprecated false
26
+
27
namespace String
28
29
-- TODO(kmill): add `@[ext]` attribute to `String.ext` in core.
lean-toolchain
@@ -1 +1 @@
1
-leanprover/lean4-pr-releases:pr-release-13254-7d41ef3
+leanprover/lean4-pr-releases:pr-release-13254-1d0d0c4
0 commit comments