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