Since ≡ is already taken, what would be the canonical symbol to use for equivalence (specifically a conversion)?
equivalence of what?
Equivalence of two terms in propositional logic.
Is there a specific context? Rewriting? Logical equivalence? Some arbitrary equivalence relation?
It's rewriting based. I want to represent Isabelle/ML conversions in HOL.
First of all, you should think about whether you need notation for this at all
if you do, I guess you could do something like ≡ with an aptly chosen index
Ah right, I forgot about indexing. I do think that it is necessary because I also need a proof system (with proof terms that are a HOL datatype) that certifies those conversions.
Sorry, I misunderstood you. The notation is of course not necessary. But it is nice for presentation.
Then consider deleting it after you're done
or making it optionally possible to enable/disable it with bundles
syntax is global and in my opinion people tend to overuse custom syntax
that's okay if your stuff is unlikely to ever be used by other developments, but otherwise it can be problematic
e.g. there are about three different theories in Isabelle that use "$" as a binary operator
if you import more than one of them at the same time, all hell breaks loose
Thanks, I will definitely keep that in mind for when it comes to that point :D
Last updated: Sep 25 2022 at 23:25 UTC