Zulip Chat Archive

Stream: general

Topic: Simp bug


view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Rob Lewis (Apr 25 2019 at 14:43):

Hmm, it's not use_axioms.


Last updated: May 16 2021 at 05:21 UTC