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

chore: increase threshold for Windows workaround in the previous commit

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-15 21:15:37 -07:00
parent 19d994b350
commit 5d305faee0
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/typeclass_coerce.lean
View file

@ -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)

2
tests/lean/run/typeclass_diamond.lean
View file

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