`omega` has issues with `mdata` handling
girving opened this issue · 1 comments
girving commented
This MWE is from Damiano Testa, and I've hit it in the wild in other cases:
import Std.Tactic.Omega
example : 0 = 0 := by
have : 0 = 0 := by omega -- works
omega -- fails
He suggests it's mdata
-related, and indeed a tactic he wrote that clears mdata
fixes the problem.