Open dranov opened 2 months ago
The change in PR #122 seems sufficient.
Hi @dranov! Thanks for filing the bug and working on a fix. While your PR is sound, the proof reconstruction part of the tactic is not aware of the change, which might cause Lean to reject the reconstructed proof. To avoid confusion, it's better to eliminate Iff
in a pre-processing step. PR #123 addresses this for the most part, though there may still be some corner cases. We'll have a proper solution once we start integrating lean-smt
with lean-auto
.
That makes sense. Thank you for the quick fix!
The generated query is:
which returns
sat