Skip to content

Commit ad66ab4

Browse files
committed
workaround for stage 3
1 parent 8e871fb commit ad66ab4

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/Init/Data/Vector/Extract.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@ prelude
99
import Init.Data.Vector.Lemmas
1010
import Init.Data.Array.Extract
1111

12+
set_option maxHeartbeats 20000000
13+
1214
/-!
1315
# Lemmas about `Vector.extract`
1416
-/

0 commit comments

Comments
 (0)