*To*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Subject*: Re: [isabelle] A special notation for function application*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Thu, 04 Aug 2011 14:23:52 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAL0S8BeLkLWV7TiCyThWntArqn5nt41hEd+mWbOQJmHSyOuLxQ@mail.gmail.com>*References*: <CAL0S8BeLkLWV7TiCyThWntArqn5nt41hEd+mWbOQJmHSyOuLxQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.13) Gecko/20101208 Thunderbird/3.1.7

Dear Jesus,

abbreviation (input) app :: "('b => 'a) => 'b => 'a" ("<(_),(_)>" 90) where "<f, x> == f x" term "<f, x>"

Hope this helps, Andreas Am 04.08.2011 13:55, schrieb Jesus Aransay:

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

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 031 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**References**:**[isabelle] A special notation for function application***From:*Jesus Aransay

- Previous by Date: [isabelle] A special notation for function application
- Next by Date: [isabelle] Accessing (individual) simplification rules of function definitions
- Previous by Thread: [isabelle] A special notation for function application
- Next by Thread: [isabelle] Accessing (individual) simplification rules of function definitions
- Cl-isabelle-users August 2011 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