- lambda_delta: static type assignment is defined

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / basic_1.txt

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index 5370377e61f77a679460b2d8278829b6927a56ce..1b6aaa13f0d78844cee8fbe7d9a5bfe6080fc8aa 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -47,9 +47,6 @@ asucc/fwd asucc_gen_head
 cnt/props cnt_lift
 C/props clt_wf__q_ind
 C/props clt_wf_ind
-C/props chead_ctail
-C/props clt_thead (ctail)
-C/props c_tail_ind
 csuba/arity csuba_arity
 csuba/arity csuba_arity_rev
 csuba/arity arity_appls_appl
@@ -103,7 +100,6 @@ csubv/getl csubv_getl_conf_void
 csubv/props csubv_bind_same
 csubv/props csubv_refl
 drop1/props drop1_cons_tail
-drop/props drop_ctail
 ex0/props aplus_gz_le
 ex0/props aplus_gz_ge
 ex0/props next_plus_gz
@@ -132,18 +128,10 @@ leq/props leq_trans
 leq/props leq_ahead_false_1
 leq/props leq_ahead_false_2
 lift1/fwd lift1_cons_tail
-
-# check #############################################################
-
-lift1/fwd lifts1_flat
 lift1/fwd lifts1_nil
 lift1/fwd lifts1_cons
-lift1/props lift1_free
 lift/props thead_x_lift_y_y
 lift/props lifts_tapp
-
-# waiting ####################################################################
-
 lift/props lifts_inj
 llt/props lweight_repl
 llt/props llt_repl
@@ -156,8 +144,6 @@ next_plus/props next_plus_assoc
 next_plus/props next_plus_next
 next_plus/props next_plus_lt
 nf2/arity arity_nf2_inv_all
-nf2/dec nf2_dec
-
 nf2/fwd nf2_gen_lref
 nf2/fwd nf2_gen_abst
 nf2/fwd nf2_gen_cast
@@ -165,15 +151,9 @@ nf2/fwd nf2_gen_beta
 nf2/fwd nf2_gen_flat
 nf2/fwd nf2_gen__nf2_gen_aux
 nf2/fwd nf2_gen_abbr
-
 nf2/fwd nf2_gen_void
-nf2/iso nf2_iso_appls_lref
-nf2/pr3 nf2_pr3_unfold
-nf2/pr3 nf2_pr3_confluence
-
 nf2/props nfs2_tapp
 nf2/props nf2_appls_lref
-
 pc1/props pc1_pr0_r
 pc1/props pc1_pr0_x
 pc1/props pc1_refl
@@ -190,51 +170,22 @@ pc3/dec pc3_abst_dec
 pc3/fsubst0 pc3_pr2_fsubst0
 pc3/fsubst0 pc3_pr2_fsubst0_back
 pc3/fsubst0 pc3_fsubst0
-pc3/fwd pc3_gen_sort
-pc3/fwd pc3_gen_abst
-pc3/fwd pc3_gen_abst_shift
-pc3/fwd pc3_gen_lift
 pc3/fwd pc3_gen_not_abst
 pc3/fwd pc3_gen_lift_abst
-pc3/fwd pc3_gen_sort_abst
-pc3/left pc3_ind_left__pc3_left_pr3
-pc3/left pc3_ind_left__pc3_left_trans
-pc3/left pc3_ind_left__pc3_left_sym
-pc3/left pc3_ind_left__pc3_left_pc3
-pc3/left pc3_ind_left__pc3_pc3_left
-pc3/left pc3_ind_left
 pc3/nf2 pc3_nf2
 pc3/nf2 pc3_nf2_unfold
 pc3/pc1 pc3_pc1
-pc3/props pc3_pr2_r
-pc3/props pc3_pr2_x
-pc3/props pc3_pr3_r
-pc3/props pc3_pr3_x
-pc3/props pc3_pr3_t
-pc3/props pc3_s
-pc3/props pc3_thin_dx
-pc3/props pc3_head_1
-pc3/props pc3_head_2
-pc3/props pc3_pr2_u
-pc3/props pc3_t
-pc3/props pc3_pr2_u2
-pc3/props pc3_pr3_conf
-pc3/props pc3_head_12
-pc3/props pc3_head_21
 pc3/props pc3_pr0_pr2_t
 pc3/props pc3_pr2_pr2_t
 pc3/props pc3_pr2_pr3_t
 pc3/props pc3_pr3_pc3_t
-pc3/props pc3_lift
 pc3/props pc3_eta
 pc3/subst1 pc3_gen_cabbr
 pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
 pc3/wcpr0 pc3_wcpr0_t
 pc3/wcpr0 pc3_wcpr0
-pr0/fwd pr0_gen_void
-
-# check #############################################################
 
+pr0/fwd pr0_gen_void
 pr0/dec nf0_dec
 pr0/subst1 pr0_subst1_back
 pr0/subst1 pr0_subst1_fwd
@@ -246,39 +197,13 @@ pr1/props pr1_head_1
 pr1/props pr1_head_2
 pr1/props pr1_comp
 pr1/props pr1_eta
-pr2/clen pr2_gen_ctail
 pr2/fwd pr2_gen_void
-pr2/props pr2_ctail
 pr2/subst1 pr2_gen_cabbr
 pr3/fwd pr3_gen_void
 pr3/pr1 pr3_pr1
-
-pr3/pr3 pr3_strip
-pr3/props pr3_thin_dx
-pr3/props pr3_head_1
-pr3/props pr3_head_2
-pr3/props pr3_head_21
-pr3/props pr3_head_12
 pr3/props pr3_eta
-pr3/subst1 pr3_subst1
 pr3/subst1 pr3_gen_cabbr
-sn3/props sn3_cpr3_trans
-
-sn3/props sn3_shift
-sn3/props sn3_change
-sn3/props sn3_gen_def
-sn3/props sn3_cdelta
-sn3/props sn3_appl_appls
-sn3/props sn3_appls_lref
 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
@@ -310,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
@@ -339,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