Zulip Chat Archive

Stream: maths

Topic: deep recursion error for squeeze_simp


view this post on Zulip Ashvni Narayanan (Feb 18 2021 at 16:59):

Hello, I just completed a proof and was trying to remove the non-terminal simps by using squeeze_simp. I get the following error:

deep recursion was detected at 'replace' (potential solution: increase stack space in your system

The proof is of exp_bernoulli_poly' in the src\number_theory\bernoulli_polynomials.lean file on the bernoulli-polynomials branch. I get the error for the simps on lines 185 and 187 (The proof is a little long).

Any help is appreciated, thank you!

view this post on Zulip Eric Wieser (Feb 18 2021 at 17:12):

Try simp?, which is less likely to fail, although more likely to not give you a complete set of lemmas

view this post on Zulip Ashvni Narayanan (Feb 18 2021 at 17:21):

Thanks! That worked for the first simp, unfortunately not for the second one (now on line 193). I guess I could try and use rw instead, now that I know the lemmas being used..

view this post on Zulip Eric Wieser (Feb 18 2021 at 17:32):

branch#bernoulli-polynomials for others trying to help


Last updated: May 11 2021 at 15:12 UTC