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



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?

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





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