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
"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