Re: [isabelle] Syntax proposal: multiway if

[Gerwin Klein <kleing at unsw.edu.au>]

I'd be against introducing another If definition. There is a lot of automation that interacts with "If", and if you maintain your own automation, you'd now have to do two sets.

Not opposed to the notation, though. If we can figure out a way to not fire for single "if P => x | otherwise => y" case that could be quite nice. It could be part of the standard If as input, and as a bundle for output.

Cheers,
Gerwin

> On 11 Feb 2021, at 06:03, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> One could of course do that. I'm not really sure it's better. I think I
> would prefer having it just as notation. But I'm not opposed to it either.
> 
> Manuel
> 
> 
> On 10/02/2021 19:59, Christian Sternagel wrote:
>> On 2/10/21 4:07 PM, 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.
>> 
>> 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).
>> 
>> cheers
>> 
>> chris
>> 
>>> 
>>> Manuel
>>> 
>> 
>

Attachment: signature.asc
Description: Message signed with OpenPGP