Skip to content

Commit 9dc1faf

Browse files
authored
chore: add an internal String function (#10635)
This PR adds an internal `String` function ahead of an upcoming PR.
1 parent 663d4d2 commit 9dc1faf

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/Init/Data/String/Bootstrap.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -122,6 +122,9 @@ opaque drop (s : String) (n : Nat) : String
122122
@[extern "lean_string_dropright"]
123123
opaque dropRight (s : String) (n : Nat) : String
124124

125+
@[extern "lean_string_get_byte_fast"]
126+
opaque getUTF8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
127+
125128
end String.Internal
126129

127130
/--

0 commit comments

Comments
 (0)