From 96c4b9ee4d1aa12a07fc5cd44bef7e019feacc6c Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 24 Nov 2025 17:50:08 +0100 Subject: [PATCH] feat: coercion from `String` to `String.Slice` (#11341) This PR adds a coercion from `String` to `String.Slice`. In our envisioned future, most functions operating on strings will accept `String.Slice` parameters by default (like `str` in Rust), and this enables calling such functions with arguments of type `String`. Closes #11298. --- src/Init/Data/String/Defs.lean | 3 +++ src/Lean/Shell.lean | 2 +- src/lake/Lake/Util/Version.lean | 2 +- 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/String/Defs.lean b/src/Init/Data/String/Defs.lean index 05fd208533..2b1e908931 100644 --- a/src/Init/Data/String/Defs.lean +++ b/src/Init/Data/String/Defs.lean @@ -421,6 +421,9 @@ def toSlice (s : String) : Slice where endExclusive := s.endPos startInclusive_le_endExclusive := by simp [Pos.le_iff, Pos.Raw.le_iff] +instance : Coe String String.Slice where + coe := String.toSlice + @[simp] theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startPos := rfl diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean index 6cf5b53dd1..af3c89ffdb 100644 --- a/src/Lean/Shell.lean +++ b/src/Lean/Shell.lean @@ -255,7 +255,7 @@ def shellMain if contents.startsWith "#lang" then let endLinePos := contents.find '\n' let langId := String.Pos.Raw.extract contents ⟨6⟩ endLinePos.offset |>.trimAscii - if langId == "lean4".toSlice then + if langId == "lean4" then pure () -- do nothing for now else IO.eprintln s!"unknown language '{langId}'\n"; diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean index 38e59744ee..6602442fc4 100644 --- a/src/lake/Lake/Util/Version.lean +++ b/src/lake/Lake/Util/Version.lean @@ -269,7 +269,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do if noOrigin then return .nightly date else if let some suffix := origin.dropPrefix? defaultOrigin then - if suffix.isEmpty || suffix == "-nightly".toSlice then + if suffix.isEmpty || suffix == "-nightly" then return .nightly date else if let some n := tag.dropPrefix? "pr-release-" then if let some n := n.toNat? then