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++:

https://github.com/EdAyers/lean/commit/3e97849d03d8f720df9cbe45c2be7e0b1246e3f5

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: Dec 20 2023 at 11:08 UTC