Nominal/Ex/LF.thy
author Christian Urban <urbanc@in.tum.de>
Fri, 27 Aug 2010 02:03:52 +0800 (2010-08-26)
changeset 2438 abafea9b39bb
parent 2436 3885dc2669f9
child 2440 0a36825b16c1
permissions -rw-r--r--
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