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.