Re: [isabelle] Operator clash for $

I would like to see the following setup:

- $ is for vector subscripting, its main use.

- When combining multiple definitions of $, it should be possible to retain one of the $ while giving new syntax to the others.

It would be suboptimal if we would need to sprinkle additional lines all over MVA to cater for potential conflicts.


On 16/06/2016 11:54, Manuel Eberl wrote:

it appears that the infix operator $ is used both for the n-th component of a
vector and the n-th coefficient of a Formal Power Series.

Since I now use both Multivariate_Analysis and Formal_Power_Series, I get lots
of syntax ambiguity warnings all the time. We should probably do something about

I see the following three options:

1. Rename one of the operators. Since Formal_Power_Series is used less than
vectors, this is probably the one to change in this case. I am not sure,
however, what it could be renamed to. The standard mathematical notation is
something like "[X^n] f", so I suppose we could go for "âX^nâ f", but I'm not
sure if that's a good idea.

2. Disable the "$" notation completely outside the FPS theory, or put it in a
locale that has to be interpreted every time one wants to use the notation. On
the down side, one still runs into problems when one wants to use the $ notation
for FPSs but has Multivariate_Analysis loaded as well. I guess one could put
both of them in locales, but I don't know if we want that.

3. Use ad-hoc Overloading, similar to what is done for monads. One could then
also use $ e.g. for the n-th coefficient of a polynomial, or perhaps even unify
the notation with the n-th element of lists and arrays etc. at some point. The
down side of this is that when there are ambiguities/type errors, the error
messages get a bit confusing.

Note that "normal" overloading does not work, since the constant would have to
have the type "'a => nat => 'b", and that means one has to write type
annotations everywhere.

Any opinions? Whatever the outcome is, I will take care of implementing it.



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

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