1 theory LFex

     2 imports "Parser"

     3 begin

     4 

     5 atom_decl name

     6 atom_decl ident

     7 

     8 nominal_datatype kind =

     9     Type

    10   | KPi "ty" n::"name" k::"kind" bind n in k

    11 and ty =

    12     TConst "ident"

    13   | TApp "ty" "trm"

    14   | TPi "ty" n::"name" t::"ty" bind n in t

    15 and trm =

    16     Const "ident"

    17   | Var "name"

    18   | App "trm" "trm"

    19   | Lam "ty" n::"name" t::"trm" bind n in t

    20 

    21 thm kind_ty_trm.supp

    22 

    23 end

    24 

    25 

    26 

    27