Nominal/Ex/CoreHaskell.thy
changeset 2095 ae94bae5bb93
parent 2083 9568f9f31822
child 2100 705dc7532ee3
equal deleted inserted replaced
2093:751d1349329b 2095:ae94bae5bb93
    16 and ty =
    16 and ty =
    17   TVar "tvar"
    17   TVar "tvar"
    18 | TC "string"
    18 | TC "string"
    19 | TApp "ty" "ty"
    19 | TApp "ty" "ty"
    20 | TFun "string" "ty_lst"
    20 | TFun "string" "ty_lst"
    21 | TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
    21 | TAll tv::"tvar" "tkind" T::"ty"  bind_set tv in T
    22 | TEq "ckind" "ty"
    22 | TEq "ckind" "ty"
    23 and ty_lst =
    23 and ty_lst =
    24   TsNil
    24   TsNil
    25 | TsCons "ty" "ty_lst"
    25 | TsCons "ty" "ty_lst"
    26 and co =
    26 and co =
    27   CVar "cvar"
    27   CVar "cvar"
    28 | CConst "string"
    28 | CConst "string"
    29 | CApp "co" "co"
    29 | CApp "co" "co"
    30 | CFun "string" "co_lst"
    30 | CFun "string" "co_lst"
    31 | CAll cv::"cvar" "ckind" C::"co"  bind cv in C
    31 | CAll cv::"cvar" "ckind" C::"co"  bind_set cv in C
    32 | CEq "ckind" "co"
    32 | CEq "ckind" "co"
    33 | CRefl "ty"
    33 | CRefl "ty"
    34 | CSym "co"
    34 | CSym "co"
    35 | CCir "co" "co"
    35 | CCir "co" "co"
    36 | CAt "co" "ty"
    36 | CAt "co" "ty"
    44   CsNil
    44   CsNil
    45 | CsCons "co" "co_lst"
    45 | CsCons "co" "co_lst"
    46 and trm =
    46 and trm =
    47   Var "var"
    47   Var "var"
    48 | K "string"
    48 | K "string"
    49 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
    49 | LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t
    50 | LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
    50 | LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t
    51 | AppT "trm" "ty"
    51 | AppT "trm" "ty"
    52 | AppC "trm" "co"
    52 | AppC "trm" "co"
    53 | Lam v::"var" "ty" t::"trm"       bind v in t
    53 | Lam v::"var" "ty" t::"trm"       bind_set v in t
    54 | App "trm" "trm"
    54 | App "trm" "trm"
    55 | Let x::"var" "ty" "trm" t::"trm" bind x in t
    55 | Let x::"var" "ty" "trm" t::"trm" bind_set x in t
    56 | Case "trm" "assoc_lst"
    56 | Case "trm" "assoc_lst"
    57 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
    57 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
    58 and assoc_lst =
    58 and assoc_lst =
    59   ANil
    59   ANil
    60 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
    60 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t