perf: optimize String.compare (#13796)

This PR optimizes `String.compare` to turn it into 1 instead of 2
`memcmp` calls.
This commit is contained in:
Henrik Böving 2026-05-20 13:57:48 +01:00 committed by GitHub
parent 34df732066
commit a3fff15212
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -28,6 +28,7 @@ namespace String
/--
Lexicographic comparison of strings
-/
@[extern "lean_string_compare"]
def compare (s₁ s₂ : @& String) : Ordering :=
compareOfLessAndEq s₁ s₂