Zulip Chat Archive

Stream: general

Topic: understanding omega


view this post on Zulip Johan Commelin (Aug 09 2019 at 10:33):

Why can omega not close this goal (I know that simpa using hx.symm does, that's not the point):

k : ,
hx : 1 * 1 + 1 * 1 + 1 = 1 * 1 * k
 k = 3

I thought that omega could deal with multiplication with constants...

view this post on Zulip Rob Lewis (Aug 09 2019 at 10:42):

@Seul Baek Judging by the error message, I think this is a bug.

view this post on Zulip Seul Baek (Aug 17 2019 at 20:03):

Fixed and made a PR. The error was due to not using one_mul and mul_one in the preprocessing step


Last updated: May 07 2021 at 00:30 UTC