Zulip Chat Archive

Stream: general

Topic: limitations of `abel`


view this post on Zulip Heather Macbeth (Jun 25 2020 at 22:31):

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

view this post on Zulip Jalex Stark (Jun 25 2020 at 22:38):

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 }

view this post on Zulip Alex J. Best (Jun 25 2020 at 23:03):

#3173 should do the trick then!


Last updated: May 12 2021 at 05:19 UTC