# [isabelle] A special notation for function application

Dear all,
I was trying to introduce some additional notation for linear
functionals in vector spaces; the idea is to use:
"[x, f]" as an alternative notation for "f x", where "f" is a linear
functional (let's say, type "'a => 'b") and "x" is an element of type
"'a" (note that the arguments f and x are interchanged in the proposed
notation).
I would like that all notation available for "f x" would still work
for the new notation "[x, f]", in such a way that
[x, f] \oplus [y, f]
would be equivalent to (without unfolding any particular definition):
f x \oplus f y
Is it possible to reach these behavior? How? Maybe brackets are
already a bit overloaded in terms of notation (lists, propositions...)
so a notation based for instance in "<x, f >" would be also
acceptable.
I tried the following approach (which does not interchange arguments)
abbreviation
app :: "('b => 'a) => 'b => 'a" ("<(_),(_)>" 90)
where "<f, x> == f x"
but then when I write, for instance, "term <f, x>" the system does not
seem to find the correct type of the expression.
Thanks for any hint,
Jesus
--
Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

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