]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
- lambda_delta: static type assignment is defined
[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / basic_1.txt
index caa897decc86453ad710da3e2ff359ae09cd5531..1b6aaa13f0d78844cee8fbe7d9a5bfe6080fc8aa 100644 (file)
@@ -204,13 +204,6 @@ pr3/pr1 pr3_pr1
 pr3/props pr3_eta
 pr3/subst1 pr3_gen_cabbr
 sn3/props sns3_lifts
-sty0/fwd sty0_gen_sort
-sty0/fwd sty0_gen_lref
-sty0/fwd sty0_gen_bind
-sty0/fwd sty0_gen_appl
-sty0/fwd sty0_gen_cast
-sty0/props sty0_lift
-sty0/props sty0_correct
 sty1/cnt sty1_cnt
 sty1/props sty1_trans
 sty1/props sty1_bind
@@ -242,11 +235,7 @@ ty3/dec ty3_inference
 ty3/fsubst0 ty3_fsubst0
 ty3/fsubst0 ty3_csubst0
 ty3/fsubst0 ty3_subst0
-ty3/fwd ty3_gen_sort
-ty3/fwd ty3_gen_lref
-ty3/fwd ty3_gen_bind
 ty3/fwd ty3_gen_appl
-ty3/fwd ty3_gen_cast
 ty3/fwd tys3_gen_nil
 ty3/fwd tys3_gen_cons
 ty3/fwd_nf2 ty3_gen_appl_nf2
@@ -271,12 +260,8 @@ ty3/pr3_props ty3_tred
 ty3/pr3_props ty3_sconv_pc3
 ty3/pr3_props ty3_sred_back
 ty3/pr3_props ty3_sconv
-ty3/props ty3_lift
-ty3/props ty3_correct
 ty3/props ty3_unique
 ty3/props ty3_gen_abst_abst
-ty3/props ty3_typecheck
-ty3/props ty3_getl_subst0
 ty3/sty0 ty3_sty0
 ty3/subst1 ty3_gen_cabbr
 ty3/subst1 ty3_gen_cvoid