corrected bug with fv-function generation (that was the problem with recursive binders)
theory LF
imports "../NewParser"
begin
declare [[STEPS = 20]]
atom_decl name
atom_decl ident
nominal_datatype kind =
Type
| KPi "ty" n::"name" k::"kind" bind n in k
and ty =
TConst "ident"
| TApp "ty" "trm"
| TPi "ty" n::"name" ty::"ty" bind n in ty
and trm =
Const "ident"
| Var "name"
| App "trm" "trm"
| Lam "ty" n::"name" t::"trm" bind n in t
(*thm kind_ty_trm.supp*)
end