*To*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Operator clash for $*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 16 Jun 2016 12:08:48 +0200*In-reply-to*: <1f1b2cf0-1da5-adf5-6fdd-277fba503f43@in.tum.de>*References*: <1f1b2cf0-1da5-adf5-6fdd-277fba503f43@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Hi Manuel,

op $\<^sub>v for vectors op $\<^sup>p for formal power series op $\<^sup>f for FinFun

[1] https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-June/006891.html Andreas On 16/06/16 11:54, Manuel Eberl wrote:

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

**References**:**[isabelle] Operator clash for $***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Operator clash for $
- Next by Date: [isabelle] Operational semantics for functional languages in Isabelle/HOL
- Previous by Thread: Re: [isabelle] Operator clash for $
- Next by Thread: Re: [isabelle] Operator clash for $
- Cl-isabelle-users June 2016 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