# [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
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