Zulip Chat Archive

Stream: general

Topic: resetI

Simon Hudon (Apr 11 2018 at 00:34):

Is there any reason resetI wouldn't work in the latest nightly? I have a very short proof with intro ; resetI in it and I get:

excessive memory consumption detected at 'vm' (potential solution: increase memory consumption threshold)

Simon Hudon (Apr 11 2018 at 00:46):

Ok, I found the problem. I had a local definition of resetI that just called mathlib's resetI but it wasn't fully qualified so it just worked as a recursive function ...

Mario Carneiro (Apr 11 2018 at 00:56):

oh thank god... fixing resetI was giving me nightmares

Simon Hudon (Apr 11 2018 at 01:03):

It doesn't seem to give you much leeway in how you use it, am I wrong?

Last updated: Aug 03 2023 at 10:10 UTC