Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Reto Kramer <kramer@acm.org>
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
use primrec.
I've scanned the tutorial, google and the reference manual, but was
unable to locate a relevant example.
Thanks,
consts matchE :: "expr \<times> expr \<Rightarrow>
bool" ("\<subseteq>E" 500) <-- prefix ok, infix though?
recdef matchE "measure (\<lambda>(e1,e2). depthE e1 + depthE e2)"
...
Email Gateway (Aug 17 2022 at 13:27):From: Norbert Schirmer <norbert.schirmer@web.de>
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
Email Gateway (Aug 17 2022 at 13:27):From: Alexander Krauss <krauss@in.tum.de>
Reto Kramer wrote:
You can only declare infix syntax for curried functions.
If you want infix syntax, you have to define an auxiliary function:
consts
matchE_aux :: "expr * expr => bool"
matchE :: "expr => expr => bool" ("\<subseteq>E" 500)
recdef matchE "measure (\<lambda>(e1,e2). depthE e1 + depthE e2)"
...
defs
matchE_def: "matchE x y == matchE_aux (x,y)"
(* now derive the recursion equations of matchE from matchE_aux ...*)
Hope this helps...
Alex
Last updated: May 03 2024 at 04:19 UTC