Lukas Stevens (Mar 18 2020 at 11:02): Lukas Stevens (Mar 18 2020 at 11:02):Since ≡ is already taken, what would be the canonical symbol to use for equivalence (specifically a conversion)?
Manuel Eberl (Mar 18 2020 at 11:07):equivalence of what?
Lukas Stevens (Mar 18 2020 at 11:10):Equivalence of two terms in propositional logic.
Josh Chen (Mar 18 2020 at 11:13):Is there a specific context? Rewriting? Logical equivalence? Some arbitrary equivalence relation?
Lukas Stevens (Mar 18 2020 at 11:14):It's rewriting based. I want to represent Isabelle/ML conversions in HOL.
Manuel Eberl (Mar 18 2020 at 11:15):First of all, you should think about whether you need notation for this at all
Manuel Eberl (Mar 18 2020 at 11:16):if you do, I guess you could do something like ≡ with an aptly chosen index
Lukas Stevens (Mar 18 2020 at 11:18):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.
Manuel Eberl (Mar 18 2020 at 11:19):So?
Lukas Stevens (Mar 18 2020 at 11:21):Sorry, I misunderstood you. The notation is of course not necessary. But it is nice for presentation.
Manuel Eberl (Mar 18 2020 at 11:27):Then consider deleting it after you're done
Manuel Eberl (Mar 18 2020 at 11:27):or making it optionally possible to enable/disable it with bundles
Manuel Eberl (Mar 18 2020 at 11:28):syntax is global and in my opinion people tend to overuse custom syntax
Manuel Eberl (Mar 18 2020 at 11:28):that's okay if your stuff is unlikely to ever be used by other developments, but otherwise it can be problematic
Manuel Eberl (Mar 18 2020 at 11:29):e.g. there are about three different theories in Isabelle that use "$" as a binary operator
Manuel Eberl (Mar 18 2020 at 11:29):if you import more than one of them at the same time, all hell breaks loose
Lukas Stevens (Mar 18 2020 at 11:51):Thanks, I will definitely keep that in mind for when it comes to that point :D
Last updated: Dec 21 2024 at 12:33 UTC