Re: [isabelle] Syntax proposal: multiway if
Maybe could go to HOL-Library ?
On Wed, 2021-02-10 at 16:07 +0100, Manuel Eberl wrote:
> 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
> 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"
> 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
> Not sure how to fix that.
This archive was generated by a fusion of
Pipermail (Mailman edition) and