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: Dec 20 2023 at 11:08 UTC