workaround for stage3

zwarich · zwarich · commit a90d5fce9520 · 2025-05-13T16:24:37.000-07:00
diff --git a/src/Init/Data/Vector/Extract.lean b/src/Init/Data/Vector/Extract.lean
@@ -9,6 +9,8 @@ prelude
 import Init.Data.Vector.Lemmas
 import Init.Data.Array.Extract
 
+set_option maxHeartbeats 20000000
+
 /-!
 # Lemmas about `Vector.extract`
 -/
