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
Last updated: Aug 03 2023 at 10:10 UTC