Nominal/Ex/CoreHaskell.thy
changeset 2424 621ebd8b13c4
parent 2410 2bbdb9c427b5
child 2428 58e60df1ff79
equal deleted inserted replaced
2420:f2d4dae2a10b 2424:621ebd8b13c4
    18 and ty =
    18 and ty =
    19   TVar "tvar"
    19   TVar "tvar"
    20 | TC "string"
    20 | TC "string"
    21 | TApp "ty" "ty"
    21 | TApp "ty" "ty"
    22 | TFun "string" "ty_lst"
    22 | TFun "string" "ty_lst"
    23 | TAll tv::"tvar" "tkind" T::"ty"  bind_set tv in T
    23 | TAll tv::"tvar" "tkind" T::"ty"  bind (set) tv in T
    24 | TEq "ckind" "ty"
    24 | TEq "ckind" "ty"
    25 and ty_lst =
    25 and ty_lst =
    26   TsNil
    26   TsNil
    27 | TsCons "ty" "ty_lst"
    27 | TsCons "ty" "ty_lst"
    28 and co =
    28 and co =
    29   CVar "cvar"
    29   CVar "cvar"
    30 | CConst "string"
    30 | CConst "string"
    31 | CApp "co" "co"
    31 | CApp "co" "co"
    32 | CFun "string" "co_lst"
    32 | CFun "string" "co_lst"
    33 | CAll cv::"cvar" "ckind" C::"co"  bind_set cv in C
    33 | CAll cv::"cvar" "ckind" C::"co"  bind (set) cv in C
    34 | CEq "ckind" "co"
    34 | CEq "ckind" "co"
    35 | CRefl "ty"
    35 | CRefl "ty"
    36 | CSym "co"
    36 | CSym "co"
    37 | CCir "co" "co"
    37 | CCir "co" "co"
    38 | CAt "co" "ty"
    38 | CAt "co" "ty"
    46   CsNil
    46   CsNil
    47 | CsCons "co" "co_lst"
    47 | CsCons "co" "co_lst"
    48 and trm =
    48 and trm =
    49   Var "var"
    49   Var "var"
    50 | K "string"
    50 | K "string"
    51 | LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t
    51 | LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t
    52 | LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t
    52 | LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t
    53 | AppT "trm" "ty"
    53 | AppT "trm" "ty"
    54 | AppC "trm" "co"
    54 | AppC "trm" "co"
    55 | Lam v::"var" "ty" t::"trm"       bind_set v in t
    55 | Lam v::"var" "ty" t::"trm"       bind (set) v in t
    56 | App "trm" "trm"
    56 | App "trm" "trm"
    57 | Let x::"var" "ty" "trm" t::"trm" bind_set x in t
    57 | Let x::"var" "ty" "trm" t::"trm" bind (set) x in t
    58 | Case "trm" "assoc_lst"
    58 | Case "trm" "assoc_lst"
    59 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
    59 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
    60 and assoc_lst =
    60 and assoc_lst =
    61   ANil
    61   ANil
    62 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
    62 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t