]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0f34e7f) | patch
- some work on extensions:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 10 Apr 2014 20:50:46 +0000 (20:50 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 10 Apr 2014 20:50:46 +0000 (20:50 +0000)
commit890a19d326338d96879dedce1eadc7c91a3beac2
tree5065399077df33c473bf7df1b19a31a27facff21tree | snapshot
parent0f34e7f3ada66fdc9044b5ed5c5f59ea36d3c6a2commit | diff
- some work on extensions:
  the alternative definition of lpx_sn and llpx_sn is useless since it is recursive
  llor seems to contain a bug in the referred components
- some work pointwise extended reduction:
  we restore the "full" version and use it for the normaliztion of extended reduction
  we still use "lazy" version for the "big-tree" theorem
48 files changed:
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.