max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: increase synthInstance.maxHeartbeats default

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-04 17:34:57 -08:00
parent 73e718c5eb
commit e415cfa632
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/SynthInstance.lean
View file

@ -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"
}