Re: [isabelle] Notation for series coefficients



Hm, I think the usual option is to just go with a new $ notation. Maybe
using context/private notation tricks?

Alternatively, you could also try to use the coercion from 'a egf to 'a
fps, and then introduce a output abbreviation:
  f $_fps x == fps_of_egf f $ x

 - Johannes



Am Mittwoch, den 16.09.2015, 10:53 +0200 schrieb Manuel Eberl:
> Hallo,
> 
> I am currently thinking about introducing a type 'a egf for exponential 
> generating functions, derived from formal power series ('a fps).
> 
> I was wondering how to best express the n-th coefficient of an egf. For 
> polynomials, only the rather unwieldy notation "coeff f n" exists. For 
> formal power series, "f $ n" exists.
> 
> I considered overloading the $ notation so that it works for 
> polynomials, formal power series, and exponential generating functions. 
> However:
> â introducing a typeclass does not work, because this would be a 
> higher-order typeclass.
> â Vanilla âoverloadingâ works, but the type of "op $" must then be 'a â 
> nat â 'b, which means that type inference cannot deduce the result type 
> of "f $ 0" even when the type of "f" is known, requiring type 
> annotations everywhere.
> â Adhoc overloading would probably work, but that is somewhatâ ad-hoc.
> 
> Does anybody have other ideas?
> 
> 
> Manuel
> 






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