limitations of `abel`

Stream: general

[Heather Macbeth]

Perhaps this is well known, but I was surprised at something abel could not do.

import tactic.abel
variables (G : Type) [add_comm_group G]

-- works
example (x : G) : x + 0 = x := by abel

-- fails
example (x : G) : x - 0 = x := by abel

[Jalex Stark]

i don't know why abel wants to convert (-0) into (-1) •ℤ 0 given that it doesn't know gsmul_zero

example (x : G) : x - 0 = x := by { abel, rw gsmul_zero, abel }

[Alex J. Best]

#3173 should do the trick then!