theory SystemFOmega
imports "../Nominal2"
begin

text {*
  System from the F-ing paper by Rossberg, Russo and 
  Dreyer, TLDI'10
*}


atom_decl var
atom_decl tvar
atom_decl label

nominal_datatype kind =
  \<Omega> | KFun kind kind

nominal_datatype ty =
  TVar tvar
| TFun ty ty
| TAll a::tvar kind t::ty bind a in t
| TEx  a::tvar kind t::ty bind a in t
| TLam a::tvar kind t::ty bind a in t
| TApp ty ty
| TRec trec
and trec =
  TRNil
| TRCons label ty trec 

nominal_datatype trm =
  Var var
| Lam x::var ty t::trm bind x in t
| App trm trm
| Dot trm label
| LAM a::tvar kind t::trm bind a in t
| APP trm ty
| Pack ty trm
| Unpack a::tvar x::var trm t::trm bind a x in t
| Rec rec 
and rec =
  RNil
| RCons label trm rec




end