Re: [isabelle] recdef tuple for 2 args, infix syntax possible?

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)

"e1 \<subseteq>E e2" == "matchE (e1, e2)"

term "e1 \<subseteq>E e2"

You can also define the E as subscript.


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