Commit 2020-05-25 07:24 a3b3aa62

fix(tactic/norm_num): workaround int.sub unfolding bug (#2804) Fixes https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/certificates.20for.20calculations/near/198631936 . Or rather, it works around an issue in how the kernel unfolds applications. The real fix is probably to adjust the definitional height or other heuristics around add_group_has_sub and int.sub so that tries to prove that they are defeq that way rather than unfolding bit0 and bit1. Here is a MWE for the issue:

example : int.has_sub = add_group_has_sub := rfl
example :
  (@has_sub.sub ℤ int.has_sub 5000 2 : ℤ) =
  (@has_sub.sub ℤ add_group_has_sub 5000 2) := rfl -- deep recursion