theory LetFun
imports "../Nominal2"
begin

atom_decl name

(* x is bound in both e1 and e2
   names in p are bound only in e1 *)

nominal_datatype exp =
  Var name
| Pair exp exp
| LetRec x::name p::pat e1::exp e2::exp  bind x in e2, bind x "bp p" in e1
and pat =
  PVar name
| PUnit
| PPair pat pat
binder
  bp :: "pat \<Rightarrow> atom list"
where
  "bp (PVar x) = [atom x]"
| "bp (PUnit) = []"
| "bp (PPair p1 p2) = bp p1 @ bp p2"

end