From 5d305faee0db4bd28095a172e332eaf28571a781 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 May 2021 21:15:37 -0700 Subject: [PATCH] chore: increase threshold for Windows workaround in the previous commit --- tests/lean/run/typeclass_coerce.lean | 2 +- tests/lean/run/typeclass_diamond.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean index a3ce37dbae..b72ecd4582 100644 --- a/tests/lean/run/typeclass_coerce.lean +++ b/tests/lean/run/typeclass_coerce.lean @@ -71,7 +71,7 @@ axiom Top (α : Type) (n : Nat) : Type #print "-----" set_option synthInstance.maxSize 256 -set_option synthInstance.maxHeartbeats 5000 +set_option synthInstance.maxHeartbeats 500000 #synth HasCoerce (Top Unit Nat.zero) (Top Unit Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ) diff --git a/tests/lean/run/typeclass_diamond.lean b/tests/lean/run/typeclass_diamond.lean index 403a06a2a5..99a184edce 100644 --- a/tests/lean/run/typeclass_diamond.lean +++ b/tests/lean/run/typeclass_diamond.lean @@ -27,7 +27,7 @@ class Top (n : Nat) : Type := (u : Unit := ()) instance Top₁ToTop (n : Nat) [Top₁ n] : Top n := {} instance Top₂ToTop (n : Nat) [Top₂ n] : Top n := {} -set_option synthInstance.maxHeartbeats 500 +set_option synthInstance.maxHeartbeats 5000 #synth Top Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ