matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda_delta/basic_2/computation/csn

]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Thu, 19 Jul 2012 13:52:06 +0000 (13:52 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Thu, 19 Jul 2012 13:52:06 +0000 (13:52 +0000)
commit	5ea90cbbb01fe0bf3b77221d9e6c87002982621f
tree	cbce810919a818e81a754ac3af0d05fb298d013a	tree \| snapshot
parent	2f0626b0315cb0ca51aacb40234f02edd970524c	commit \| diff

- intermediate commit to allow debugging of auto tactic in xprs.ma
- extended computation is now defined (its De Vrijer's reduction rt)
- stratified native validity is now defined (it's supposed to be
easier to deal with than native type assignment)

40 files changed:

matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/notation.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom