search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

A different operator precedence when parsing HOL? #553

Closed quickbeam123 closed 4 months ago

quickbeam123 commented 6 months ago

Geoff writes:

Part of the cause of this confusion is that Vampire (and E) still parses ...
    ! [X:$o] : X = X
... incorrectly, as ...
    (! [X:$o] : X) = X
...
<and explains that uses a workaround for now, to always create     ! [X:$o] : (X = X) for us>
...
deep in your heart, don't you want to do the right thing and fix the parsing?

I guess the fix requires making sure that = binds stronger than a quantifier?

MichaelRawson commented 4 months ago

This caused some e-mail discussion and last I heard Geoff was confused about it and it needed a re-think. Closing for now.