Skip to content

Commit 157486e

Browse files
committed
Oops, lost an extern annotation
1 parent 16c7442 commit 157486e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Data/String/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ where
9494
(have := c.utf8Size_pos; have := le_size_of_utf8DecodeChar?_eq_some h; by omega)
9595
termination_by structural fuel
9696

97-
@[inline, expose]
97+
@[expose, extern "lean_string_validate_utf8"]
9898
def ByteArray.validateUTF8 (b : ByteArray) : Bool :=
9999
go (b.size + 1) 0 (by simp) (by simp)
100100
where

0 commit comments

Comments
 (0)