Nominal/ExCoreHaskell.thy
changeset 1699 2dca07aca287
parent 1698 69472e74bd3b
child 1700 b5141d1ab24f
equal deleted inserted replaced
1698:69472e74bd3b 1699:2dca07aca287
    27 | TEq "ckind" "ty"
    27 | TEq "ckind" "ty"
    28 and ty_lst =
    28 and ty_lst =
    29   TsNil
    29   TsNil
    30 | TsCons "ty" "ty_lst"
    30 | TsCons "ty" "ty_lst"
    31 and co =
    31 and co =
    32   CC cvar
    32   CVar "cvar"
    33 | CConst "string"
    33 | CConst "string"
    34 | CApp "co" "co"
    34 | CApp "co" "co"
    35 | CFun "string" "co_lst"
    35 | CFun "string" "co_lst"
    36 | CAll tv::"tvar" "ckind" C::"co"  bind tv in C
    36 | CAll cv::"cvar" "ckind" C::"co"  bind cv in C
    37 | CEq "ckind" "co"
    37 | CEq "ckind" "co"
    38 | CRefl "ty"
    38 | CRefl "ty"
    39 | CSym "co"
    39 | CSym "co"
    40 | CCir "co" "co"
    40 | CCir "co" "co"
    41 | CAt "co" "ty"
    41 | CAt "co" "ty"
    48 and co_lst =
    48 and co_lst =
    49   CsNil
    49   CsNil
    50 | CsCons "co" "co_lst"
    50 | CsCons "co" "co_lst"
    51 and trm =
    51 and trm =
    52   Var "var"
    52   Var "var"
    53 | C "string"
    53 | K "string"
    54 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
    54 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
    55 | LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
    55 | LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
    56 | AppT "trm" "ty"
    56 | AppT "trm" "ty"
    57 | AppC "trm" "co"
    57 | AppC "trm" "co"
    58 | Lam v::"var" "ty" t::"trm"       bind v in t
    58 | Lam v::"var" "ty" t::"trm"       bind v in t
    62 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
    62 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
    63 and assoc_lst =
    63 and assoc_lst =
    64   ANil
    64   ANil
    65 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
    65 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
    66 and pat =
    66 and pat =
    67   K "string" "tvtk_lst" "tvck_lst" "vt_lst"
    67   Kpat "string" "tvtk_lst" "tvck_lst" "vt_lst"
    68 and vt_lst =
    68 and vt_lst =
    69   VTNil
    69   VTNil
    70 | VTCons "var" "ty" "vt_lst"
    70 | VTCons "var" "ty" "vt_lst"
    71 and tvtk_lst =
    71 and tvtk_lst =
    72   TVTKNil
    72   TVTKNil