Re: [isabelle] Syntax proposal: multiway if

On 2/10/21 4:07 PM, 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" 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.

Dear Manuel,

Naive question: What if you would use your own dedicated constant

definition "multi_if == If"

together with some suitable simplification rules and/or other automation?

Then users could decide on their own which syntax to use (for input and output).




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