## Stream: general

### Topic: Deterministic timeout

#### 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?

#### 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).

#### Heather Macbeth (Nov 25 2020 at 04:50):

Thanks!

Last updated: May 13 2021 at 06:15 UTC