missing functionality in abel

Stream: metaprogramming / tactics

[Scott Morrison]

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]

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