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.
This commit is contained in:
Markus Himmel 2025-11-24 17:50:08 +01:00 committed by GitHub
parent fa67f300f6
commit 96c4b9ee4d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 5 additions and 2 deletions

View file

@ -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

View file

@ -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";

View file

@ -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