changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
theory LF
imports "../NewParser"
begin
declare [[STEPS = 9]]
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" t::"ty" bind n in t
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