[isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Tobias Nipkow]

The "op" noation is idiosyncratic, but there are examples (not in individual 
formulae) where I find some such notation convenient. I would welcome Haskell's 
"(+)", but that has a problem with "(*)". Unless we can make that notation work, 
I don't think we profit much by a change. Hence I am inclined to leave things as 
they are.

Tobias

On 22/09/2015 16:21, Florian Haftmann wrote:
> The »op •« is infamous. Whatever you wish instead (my personal favorite
> being no special syntax at all), problems include
> a) to detect unintended printing behaviour
> b) a suitable migration mechanisms
>
> Concerning b), one you could imagine things like
> a) alternative declarations (infix(l/r)_new beside infix(l/r),
> infix(l/r) beside infix(l/r)_old)
> b) a flag to control the semantics of infix(l/r)
> c) a flag combined with a data slot to modify existing mixfix
> declarations afterwards also
>
> Personally I would appreciate some move here, but this only makes sense
> if we agree what the goal is and whether it is worth the effort.
>
> Cheers,
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150922/f0386bad/attachment.bin>