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)