Pretty chained if syntax

[mn200]

From the Isabelle mailing list (at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-February/msg00034.html)

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.

As Manuel's message says, there's also the issue of whether or not the printer should print this syntax back or not. In HOL4, we'd probably want to have the leading pipe symbol be optional, as with our case syntax.