From 59949f89ee75fbff8271546fc6c3ab1911d248ee Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 19 Nov 2025 09:05:28 +0100 Subject: [PATCH] chore: add function `String.Pos.extract` (#11251) This PR is a preparatory bootstrapping PR for #11240. --- src/Init/Data/String/Basic.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 7130e9e7bd..3bb26cb66c 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -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 :=