Nominal/Ex/CoreHaskell.thy
changeset 2950 0911cb7bf696
parent 2630 8268b277d240
equal deleted inserted replaced
2949:adf22ee09738 2950:0911cb7bf696
    17 and ty =
    17 and ty =
    18   TVar "tvar"
    18   TVar "tvar"
    19 | TC "string"
    19 | TC "string"
    20 | TApp "ty" "ty"
    20 | TApp "ty" "ty"
    21 | TFun "string" "ty_lst"
    21 | TFun "string" "ty_lst"
    22 | TAll tv::"tvar" "tkind" T::"ty"  bind (set) tv in T
    22 | TAll tv::"tvar" "tkind" T::"ty"  binds (set) tv in T
    23 | TEq "ckind" "ty"
    23 | TEq "ckind" "ty"
    24 and ty_lst =
    24 and ty_lst =
    25   TsNil
    25   TsNil
    26 | TsCons "ty" "ty_lst"
    26 | TsCons "ty" "ty_lst"
    27 and co =
    27 and co =
    28   CVar "cvar"
    28   CVar "cvar"
    29 | CConst "string"
    29 | CConst "string"
    30 | CApp "co" "co"
    30 | CApp "co" "co"
    31 | CFun "string" "co_lst"
    31 | CFun "string" "co_lst"
    32 | CAll cv::"cvar" "ckind" C::"co"  bind (set) cv in C
    32 | CAll cv::"cvar" "ckind" C::"co"  binds (set) cv in C
    33 | CEq "ckind" "co"
    33 | CEq "ckind" "co"
    34 | CRefl "ty"
    34 | CRefl "ty"
    35 | CSym "co"
    35 | CSym "co"
    36 | CCir "co" "co"
    36 | CCir "co" "co"
    37 | CAt "co" "ty"
    37 | CAt "co" "ty"
    45   CsNil
    45   CsNil
    46 | CsCons "co" "co_lst"
    46 | CsCons "co" "co_lst"
    47 and trm =
    47 and trm =
    48   Var "var"
    48   Var "var"
    49 | K "string"
    49 | K "string"
    50 | LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t
    50 | LAMT tv::"tvar" "tkind" t::"trm" binds (set) tv in t
    51 | LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t
    51 | LAMC cv::"cvar" "ckind" t::"trm" binds (set) cv in t
    52 | AppT "trm" "ty"
    52 | AppT "trm" "ty"
    53 | AppC "trm" "co"
    53 | AppC "trm" "co"
    54 | Lam v::"var" "ty" t::"trm"       bind (set) v in t
    54 | Lam v::"var" "ty" t::"trm"       binds (set) v in t
    55 | App "trm" "trm"
    55 | App "trm" "trm"
    56 | Let x::"var" "ty" "trm" t::"trm" bind (set) x in t
    56 | Let x::"var" "ty" "trm" t::"trm" binds (set) x in t
    57 | Case "trm" "assoc_lst"
    57 | Case "trm" "assoc_lst"
    58 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
    58 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
    59 and assoc_lst =
    59 and assoc_lst =
    60   ANil
    60   ANil
    61 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
    61 | ACons p::"pat" t::"trm" "assoc_lst" binds "bv p" in t
    62 and pat =
    62 and pat =
    63   Kpat "string" "tvars" "cvars" "vars"
    63   Kpat "string" "tvars" "cvars" "vars"
    64 and vars =
    64 and vars =
    65   VsNil
    65   VsNil
    66 | VsCons "var" "ty" "vars"
    66 | VsCons "var" "ty" "vars"