One could of course do that. I'm not really sure it's better. I think I would prefer having it just as notation. But I'm not opposed to it either. Manuel On 10/02/2021 19:59, Christian Sternagel wrote: > On 2/10/21 4:07 PM, Manuel Eberl wrote: >> Hello, >> >> there is a Haskell extension that allows writing nested ifs in the >> following nice syntax: >> >> if | P -> a >> | Q -> b >> | R -> c >> | otherwise -> d >> >> I asked around and some people (e.g. Tobias Nipkow) agree that this >> might be nice to have. My proposed syntax is inspired by the "case" >> syntax and looks like this: >> >> if P ⇒ x | Q ⇒ y | R ⇒ z | otherwise ⇒ u >> >> One could also do >> >> if P ⇒ x | Q ⇒ y | R ⇒ z | _ ⇒ u >> >> instead. >> >> I attached a small theory that implements this. >> >> Not sure if this should be enabled for output by default as well – >> probably not. One could switch it on only in a special "multi_if" print >> mode, similarly to "do_notation" for monad syntax. >> >> The current implementation has the problem that "if b then x else y" >> gets output as "if b ⇒ x | otherwise ⇒ y", which we clearly don't want. >> Not sure how to fix that. > > Dear Manuel, > > Naive question: What if you would use your own dedicated constant > > definition "multi_if == If" > > together with some suitable simplification rules and/or other automation? > > Then users could decide on their own which syntax to use (for input and > output). > > cheers > > chris > >> >> Manuel >> >
Attachment:
smime.p7s
Description: S/MIME Cryptographic Signature