Topic: deep recursion
Johan Commelin (Mar 12 2019 at 13:11):
How can I debug the following error?
deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
It showed up while trying to define a class. As far as I can see there is no loop or something...
Kenny Lau (Mar 12 2019 at 13:15):
have you tried turning Lean off and on again?
Johan Commelin (Mar 12 2019 at 13:15):
Yes, in fact I have.
Johan Commelin (Mar 12 2019 at 14:07):
I've found the culprit:
-- somewhere in the perfectoid project local attribute [instance] topological_add_group.to_uniform_space
Johan Commelin (Mar 12 2019 at 14:18):
I've now put a
section ... end around this attribute (and its one use) and the problem is gone.
So... this question is solved. Thanks for letting me rubber-duck this issue!
Last updated: May 08 2021 at 11:09 UTC