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+ −