From e76eb6fbd218887f3d5f631d153e774ac7832e2b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 8 Apr 2025 11:37:33 +0200
Subject: [PATCH] fix: make Array.emptyWithCapacity actually allocate (#7869)

This PR fixes a regression introduced in #7445 where the new
`Array.emptyWithCapacity` was accidentally not tagged with the correct
function to actually allocate the capacity.
---
 src/Init/Prelude.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 3b1ee1bc1a..02b7fae052 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2932,11 +2932,10 @@ This will be deprecated in favor of `Array.emptyWithCapacity` in the future.
 def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
   toList := List.nil
 
-
-set_option linter.unusedVariables false in
 /--
 Constructs a new empty array with initial capacity `c`.
 -/
+@[extern "lean_mk_empty_array_with_capacity"]
 def Array.emptyWithCapacity {α : Type u} (c : @& Nat) : Array α where
   toList := List.nil