[isabelle] recdef tuple for 2 args, infix syntax possible?
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?
Ideally I'd like to write "x \<subseteq>E y" as if I had been able to
I've scanned the tutorial, google and the reference manual, but was
unable to locate a relevant example.
consts matchE :: "expr \<times> expr \<Rightarrow>
bool" ("\<subseteq>E" 500) <-- prefix ok, infix though?
recdef matchE "measure (\<lambda>(e1,e2). depthE e1 + depthE e2)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and