1 theory LetFun

     2 imports "../Nominal2"

     3 begin

     4 

     5 atom_decl name

     6 

     7 (* x is bound in both e1 and e2

     8    names in p are bound only in e1 *)

     9 

    10 nominal_datatype exp =

    11   Var name

    12 | Pair exp exp

    13 | LetRec x::name p::pat e1::exp e2::exp  bind x in e2, bind x "bp p" in e1

    14 and pat =

    15   PVar name

    16 | PUnit

    17 | PPair pat pat

    18 binder

    19   bp :: "pat \<Rightarrow> atom list"

    20 where

    21   "bp (PVar x) = [atom x]"

    22 | "bp (PUnit) = []"

    23 | "bp (PPair p1 p2) = bp p1 @ bp p2"

    24 

    25 end