From c2b35a89f5bcdf0592297415966dbf007f76db28 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Sep 2020 17:30:29 -0700 Subject: [PATCH] chore: increase fuel to make sure test works --- tests/lean/run/typeclass_coerce.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean index b05ea9256e..efe4c5293b 100644 --- a/tests/lean/run/typeclass_coerce.lean +++ b/tests/lean/run/typeclass_coerce.lean @@ -67,6 +67,8 @@ axiom Top (α : Type) (n : Nat) : Type #print "-----" +set_option synthInstance.maxSteps 10000 + #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)