# [isabelle] Operator clash for $

Hallo,

`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 this.
`
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.
Cheers,
Manuel

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