*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Syntax proposal: multiway if*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Wed, 10 Feb 2021 19:59:11 +0100*In-reply-to*: <4d2a929d-4ddb-2b7e-0de5-a243f61e241a@in.tum.de>*References*: <4d2a929d-4ddb-2b7e-0de5-a243f61e241a@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.0

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?

cheers chris

Manuel

**Follow-Ups**:**Re: [isabelle] Syntax proposal: multiway if***From:*Manuel Eberl

**References**:**[isabelle] Syntax proposal: multiway if***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Syntax proposal: multiway if
- Next by Date: Re: [isabelle] Syntax proposal: multiway if
- Previous by Thread: Re: [isabelle] Syntax proposal: multiway if
- Next by Thread: Re: [isabelle] Syntax proposal: multiway if
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list