1 theory ExLF

     2 imports "../NewParser"

     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_set n in k

    11 and ty =

    12     TConst "ident"

    13   | TApp "ty" "trm"

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

    15 and trm =

    16     Const "ident"

    17   | Var "name"

    18   | App "trm" "trm"

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

    20 

    21 thm kind_ty_trm.supp

    22 

    23 declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]

    24 declare alpha_gen_eqvt[eqvt]

    25 

    26 equivariance alpha_trm_raw

    27 

    28 

    29 

    30 

    31 end

    32 

    33 

    34 

    35