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:

  matchE_aux :: "expr * expr =>  bool"

  matchE :: "expr => expr => bool"  ("\<subseteq>E" 500)

recdef matchE "measure (\<lambda>(e1,e2). depthE e1 + depthE e2)"

  matchE_def: "matchE x y == matchE_aux (x,y)"

(* now derive the recursion equations of matchE from matchE_aux ...*)

Hope this helps...


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