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
use_axioms iirc, but I'm not confident there).
Rob Lewis (Apr 25 2019 at 14:43):
Hmm, it's not
Last updated: May 16 2021 at 05:21 UTC