Zulip Chat Archive

Stream: general

Topic: adding a simp_lemmas method to Lean C++

Edward Ayers (Dec 12 2018 at 16:37):

Dear lean developers. I wanted to be able to use simp_lemmas.rewrite but instead of just returning the first rewrite that worked, I want all possible rewrites. I couldn't think of a nice way to do that in Lean code so I hacked the C++:


From doing some simple tests the code works.
If any of the Lean developers have a spare moment, I would really appreciate any comments on the above commit, I am especially worried that I have introduced a memory leak by using buffer.

Last updated: Aug 03 2023 at 10:10 UTC