Re: [isabelle] Syntax proposal: multiway if



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: smime.p7s
Description: S/MIME Cryptographic Signature



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