# Re: [isabelle] Syntax proposal: multiway if

Maybe could go to HOL-Library ?
On Wed, 2021-02-10 at 16:07 +0100, 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.
>
> Manuel

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*