1 theory Shallow

     2 imports "../Nominal2" 

     3 begin

     4 

     5 (* 

     6   Various shallow binders

     7 *)

     8 

     9 atom_decl name

    10 

    11 text {* binding lists of names *}

    12 

    13 nominal_datatype trm1 =

    14   Var1 "name"

    15 | App1 "trm1" "trm1"

    16 | Lam1 xs::"name list" t::"trm1" bind xs in t

    17 

    18 

    19 text {* binding a finite set of names *}

    20 

    21 nominal_datatype trm2 =

    22   Var2 "name"

    23 | App2 "trm2" "trm2"

    24 | Lam2 xs::"name fset" t::"trm2" bind (set) xs in t

    25 

    26 

    27 text {* restricting a finite set of names *}

    28 

    29 nominal_datatype trm3 =

    30   Var3 "name"

    31 | App3 "trm3" "trm3"

    32 | Lam3 xs::"name fset" t::"trm3" bind (res) xs in t

    33 

    34 

    35 end

    36 

    37 

    38