*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Syntax proposal: multiway if*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 10 Feb 2021 20:03:03 +0100*In-reply-to*: <d2741e26-c649-6691-9e91-e1d5b1eb89f0@gmail.com>*References*: <4d2a929d-4ddb-2b7e-0de5-a243f61e241a@in.tum.de> <d2741e26-c649-6691-9e91-e1d5b1eb89f0@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.0

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**

**Follow-Ups**:**Re: [isabelle] Syntax proposal: multiway if***From:*Gerwin Klein

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

**Re: [isabelle] Syntax proposal: multiway if***From:*Christian Sternagel

- 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