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.

So?

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: Aug 15 2022 at 02:13 UTC