## Stream: general

### Topic: Simp bug

#### Chris Hughes (Apr 25 2019 at 14:31):

This gives me excessive memory consumption detected at 'whnf' (potential solution: increase memory consumption threshold) Does anyone else get this error?

import data.polynomial topology.instances.real topology.instances.polynomial

open polynomial

lemma poly_eq_poly (a b c x : ℝ) :
a * x^2 + b * x + c = eval x (C a * X^2 + C b * X + C c) :=
begin
simp only,

end


#### Rob Lewis (Apr 25 2019 at 14:34):

I noticed this working on the cap set proof. It's been on my list to debug properly but I haven't found the time. You can work around it by disabling one of the options to simp (use_axioms iirc, but I'm not confident there).

#### Rob Lewis (Apr 25 2019 at 14:43):

Hmm, it's not use_axioms.

Last updated: May 16 2021 at 05:21 UTC