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