Simp bug

Stream: general

[Chris Hughes]

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]

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]

Hmm, it's not use_axioms.