You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
import Mathlib
open Complex in
/--
error: failed to synthesize
AddMonoidHomClass (ℂ →*₀ ℝ) ℂ ℝ
(deterministic) timeout at 'typeclass', maximum number of heartbeats (19000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/
#guard_msgs in
set_option synthInstance.maxHeartbeats 19000 in
example (z : ℂ) : normSq (-z) = normSq z := by simp
This then gets slightly worse after leanprover/lean4#3807, and thereafter causes the simpNF linter to fail on Complex.normSq_neg.
The text was updated successfully, but these errors were encountered:
This then gets slightly worse after leanprover/lean4#3807, and thereafter causes the simpNF linter to fail on
Complex.normSq_neg
.The text was updated successfully, but these errors were encountered: