From a3fff15212d2ab0c5aa78c985b004c9e12162c25 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 20 May 2026 13:57:48 +0100
Subject: [PATCH] perf: optimize String.compare (#13796)

This PR optimizes `String.compare` to turn it into 1 instead of 2
`memcmp` calls.
---
 src/Init/Data/Ord/String.lean | 1 +
 1 file changed, 1 insertion(+)

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₂