Nominal/Ex/ExLF.thy
changeset 2093 751d1349329b
parent 2092 c0ab7451b20d
parent 2091 1f38489f1cf0
child 2094 56b849d348ae
child 2095 ae94bae5bb93
equal deleted inserted replaced
2092:c0ab7451b20d 2093:751d1349329b
     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 end
       
    24 
       
    25 
       
    26 
       
    27