Zulip Chat Archive

Stream: general

Topic: Deterministic timeout


view this post on Zulip Heather Macbeth (Nov 25 2020 at 04:33):

This gives a deterministic timeout for me:

import data.polynomial.basic

variables {F : Type*} [ring F]

example (X : polynomial F) (h : (5 : polynomial F) + 3 * X * X = 0) :
  4 + 4 * X * X = 0 :=
begin
  convert h using 1,

end

Can someone reproduce it and/or explain it?

view this post on Zulip Floris van Doorn (Nov 25 2020 at 04:44):

Without trying to reproduce this, this is probably related to #4678, and the reason is that convert tries to apply refl (which likely fails, but causes a lot of unfolding).

view this post on Zulip Heather Macbeth (Nov 25 2020 at 04:50):

Thanks!


Last updated: May 13 2021 at 06:15 UTC