## Stream: metaprogramming / tactics

### Topic: missing functionality in abel

#### Scott Morrison (Sep 30 2020 at 04:40):

It seems at the moment abel can't cope with

example {α : Type} [ring α] : 4 •ℤ (1 : α) = 4 :=
by abel

example {α : Type} [ring α] {a : α} : -1 •ℤ (2 * a) = -2 •ℤ a :=
by abel


presumably if these worked everyone would be happy?

#### Scott Morrison (Sep 30 2020 at 04:41):

Also

example {α : Type} [add_comm_group α] {x y : α} (h : false) :
x = - y :=
begin
abel,
abel, -- should fail, but instead inserts an additional 1 •ℤ

exfalso, assumption,
end


Last updated: May 09 2021 at 22:13 UTC