]> matita.cs.unibo.it Git - helm.git/commit
- firs theorems on native type assignment
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 19 Apr 2012 13:06:00 +0000 (13:06 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 19 Apr 2012 13:06:00 +0000 (13:06 +0000)
commitde64015de66a48373ade6cab7508d8f8e2c43af9
treea6fc9736dfaebc78b8255bae2e63f1de86f5314c
parent390de3f72df749a6f153e59e2620503657ce9eab
- firs theorems on native type assignment
- we removed iterated unfold on local environments
  since transitivity of this unfold is not needed so far
35 files changed:
matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma
matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma
matita/matita/contribs/lambda_delta/basic_2/native/nta.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/notation.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpsss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpsss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpsss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma [deleted file]