max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add function String.Pos.extract (#11251)

Browse source 
This PR is a preparatory bootstrapping PR for #11240.
This commit is contained in:
Markus Himmel 2025-11-19 09:05:28 +01:00 • committed by GitHub
parent 61186629d6
commit 59949f89ee
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Data/String/Basic.lean
View file

@ -822,6 +822,11 @@ def ValidPos.extract {s : @& String} (b e : @& s.ValidPos) : String where
bytes := s.bytes.extract b.offset.byteIdx e.offset.byteIdx
isValidUTF8 := b.isValidUTF8_extract e
@[extern "lean_string_utf8_extract"]
def Pos.extract {s : @& String} (b e : @& s.ValidPos) : String where
bytes := s.bytes.extract b.offset.byteIdx e.offset.byteIdx
isValidUTF8 := b.isValidUTF8_extract e
/-- Creates a `String` from a `String.Slice` by copying the bytes. -/
@[inline]
def Slice.copy (s : Slice) : String :=