## Stream: general

### 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

I've now put a section ... end around this attribute (and its one use) and the problem is gone.