leanprover-community/batteries

`omega` has issues with `mdata` handling

girving opened this issue · 1 comments

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.

Looks like this issue can be closed. #510 has been merged, and the example works now.