# [isabelle] Notation for series coefficients

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.*