Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: missing functionality in abel


view this post on Zulip 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?

view this post on Zulip 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