From e415cfa63218a1ceb45996139e71fda7bae1d00d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Feb 2021 17:34:57 -0800
Subject: [PATCH] chore: increase `synthInstance.maxHeartbeats` default

---
 src/Lean/Meta/SynthInstance.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 68916e411a..c3d4549832 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -15,7 +15,7 @@ import Lean.Util.Profile
 namespace Lean.Meta
 
 register_builtin_option synthInstance.maxHeartbeats : Nat := {
-  defValue := 300
+  defValue := 500
   descr := "maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }