Re: [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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev