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.