I'd like, in Coqide, to have the proof state not use a certain notation (but still use all others).
Is this possible?
From what I understand in the documentation, it is not possible. You might be able to play with opening/closing scopes but I'm not sure it will work, since it is stated explicitly that notations will be used for printing whenever possible.
Some tricks that might be sufficient are described here: How to disable my custom notation in Coq?
I wanted to add pointer to that answer because this question comes up first on Google.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With