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!
Eric Wieser (Feb 18 2021 at 17:12):
simp?, which is less likely to fail, although more likely to not give you a complete set of lemmas
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..
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