]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma
- intermediate commit to allow debugging of auto tactic in xprs.ma
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 19 Jul 2012 13:52:06 +0000 (13:52 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 19 Jul 2012 13:52:06 +0000 (13:52 +0000)
commit5ea90cbbb01fe0bf3b77221d9e6c87002982621f
treecbce810919a818e81a754ac3af0d05fb298d013a
parent2f0626b0315cb0ca51aacb40234f02edd970524c
- 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
matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
matita/matita/contribs/lambda_delta/basic_2/notation.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma
matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma