1 theory Terms

     2 imports Nominal "../QuotMain" "../QuotList"

     3 begin

     4 

     5 atom_decl name

     6 

     7 (* lets with binding patterns *)

     8 datatype trm1 =

     9   Vr1 "name"

    10 | Ap1 "trm1" "trm1"

    11 | Lm1 "name" "trm1"

    12 | Lt1 "bp" "trm1" "trm1"

    13 and bp =

    14   BUnit

    15 | BVr "name"

    16 | BPr "bp" "bp"

    17 

    18 (* lets with single assignments *)

    19 datatype trm2 =

    20   Vr2 "name"

    21 | Ap2 "trm2" "trm2"

    22 | Lm2 "name" "trm2"

    23 | Lt2 "assign" "trm2"

    24 and assign =

    25   As "name" "trm2"

    26 

    27 

    28 (* lets with many assignments *)

    29 datatype trm3 =

    30   Vr3 "name"

    31 | Ap3 "trm3" "trm3"

    32 | Lm3 "name" "trm3"

    33 | Lt3 "assign" "trm3"

    34 and assigns =

    35   ANil

    36 | ACons "name" "trm3" "assigns"

    37