Re: [isabelle] Syntax proposal: multiway if



It could, but I for one think something like this should either be
enabled by default or not exist at all (at least as input syntax – as
output, it is debatable).

Manuel


On 10/02/2021 16:41, Peter Lammich wrote:
> 
> 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
> 
> 

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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