Re: [isabelle] s/h: bogus proofs from e





On 05/11/2021 10:30, Jasmin Blanchette via Cl-isabelle-users wrote:

I find that meson is very sensitive to "using" lemmas vs feeding them as arguments and that sledgehammer ignores this.
Thank you for your report. Thanks to your example, I was able to track down the issue and find a solution for the Isabelle development version.

Somewhat belatedly: Why does meson ignore "using"? Shouldn't it take it into account like metis, simp etc? Does anybody feel responsible for meson?

Until your comment, I thought that meson wasn't ignoring "using", but that it was just treating it differently somehow. Now I just convinced myself on a small example that you're probably right. I'll look into it.

You are right, I should have written "seems to be ignoring" because I am not sure myself what exactly is going on. Thanks for taking a look.

Tobias

Jasmin


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.