*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] recdef tuple for 2 args, infix syntax possible?*From*: Norbert Schirmer <norbert.schirmer at web.de>*Date*: Wed, 19 Oct 2005 10:58:16 +0200*Cc*:*In-reply-to*: <0895D4C6-0775-408C-83B0-9D7E10E2FF01@acm.org>*Organization*: TU Muenchen*References*: <0895D4C6-0775-408C-83B0-9D7E10E2FF01@acm.org>*Reply-to*: schirmer at in.tum.de*Sender*: norbert.schirmer at web.de*User-agent*: KMail/1.7.2

On Tuesday 18 October 2005 19:17, Reto Kramer wrote: > Due to it's structure, I need to use recdef for the matchE function > (signature below). Since recdef takes one argument only, I had to > present it with a tuple (expr \<times> expr). > > Is there any way for me to still be able to create an infix syntax? Yes. You just have to define additional syntax and a syntax translation. consts matchE :: "'a \<times> 'a \<Rightarrow> bool" syntax "@matchE":: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<subseteq>E" 500) translations "e1 \<subseteq>E e2" == "matchE (e1, e2)" term "e1 \<subseteq>E e2" You can also define the E as subscript. \<subseteq>\<^sub>E Norbert

**References**:**[isabelle] recdef tuple for 2 args, infix syntax possible?***From:*Reto Kramer

- Previous by Date: Re: [isabelle] Metalogical "spec" not resolved automatically
- Next by Date: Re: [isabelle] Metalogical "spec" not resolved automatically
- Previous by Thread: Re: [isabelle] recdef tuple for 2 args, infix syntax possible?
- Next by Thread: [isabelle] Metalogical "spec" not resolved automatically
- Cl-isabelle-users October 2005 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