Nominal/Ex/SystemFOmega.thy
changeset 2950 0911cb7bf696
parent 2622 e6e6a3da81aa
equal deleted inserted replaced
2949:adf22ee09738 2950:0911cb7bf696
    17 | KFun kind kind
    17 | KFun kind kind
    18 
    18 
    19 nominal_datatype ty =
    19 nominal_datatype ty =
    20   TVar tvar
    20   TVar tvar
    21 | TFun ty ty
    21 | TFun ty ty
    22 | TAll a::tvar kind t::ty  bind a in t
    22 | TAll a::tvar kind t::ty  binds a in t
    23 | TEx  a::tvar kind t::ty  bind a in t
    23 | TEx  a::tvar kind t::ty  binds a in t
    24 | TLam a::tvar kind t::ty  bind a in t
    24 | TLam a::tvar kind t::ty  binds a in t
    25 | TApp ty ty
    25 | TApp ty ty
    26 | TRec trec
    26 | TRec trec
    27 and trec =
    27 and trec =
    28   TRNil
    28   TRNil
    29 | TRCons label ty trec 
    29 | TRCons label ty trec 
    30 
    30 
    31 nominal_datatype trm =
    31 nominal_datatype trm =
    32   Var var
    32   Var var
    33 | Lam x::var ty t::trm  bind x in t
    33 | Lam x::var ty t::trm  binds x in t
    34 | App trm trm
    34 | App trm trm
    35 | Dot trm label
    35 | Dot trm label
    36 | LAM a::tvar kind t::trm  bind a in t
    36 | LAM a::tvar kind t::trm  binds a in t
    37 | APP trm ty
    37 | APP trm ty
    38 | Pack ty trm
    38 | Pack ty trm
    39 | Unpack a::tvar x::var trm t::trm  bind a x in t
    39 | Unpack a::tvar x::var trm t::trm  binds a x in t
    40 | Rec rec 
    40 | Rec rec 
    41 and rec =
    41 and rec =
    42   RNil
    42   RNil
    43 | RCons label trm rec
    43 | RCons label trm rec
    44 
    44