matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 1 Apr 2017 13:03:45 +0000 (13:03 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 1 Apr 2017 13:03:45 +0000 (13:03 +0000)
commit	43998467c5ec5f1c8e1e988fc00e3255d2723ba4
tree	631fd0e8d0ff11db89d2348cb4da7599990a8474	tree \| snapshot
parent	5606bd084cbbf6c187b21ee5f523fa3b313bb9de	commit \| diff

- strongly normalizing terms form a candidate of reducibility
- one application of auto is unnecessarily slow,
a longly awaited improvement of auto is needed to solve the issue

matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt		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.

RSS Atom