diff --git a/src/Init/Data/Ord/String.lean b/src/Init/Data/Ord/String.lean index 37c46be239..3e409e970a 100644 --- a/src/Init/Data/Ord/String.lean +++ b/src/Init/Data/Ord/String.lean @@ -28,6 +28,7 @@ namespace String /-- Lexicographic comparison of strings -/ +@[extern "lean_string_compare"] def compare (s₁ s₂ : @& String) : Ordering := compareOfLessAndEq s₁ s₂