]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d1bda83) | patch
Work in Progress: Who needs binary_morphisms? Curryfication is your friend.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 3 Feb 2010 20:03:57 +0000 (20:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 3 Feb 2010 20:03:57 +0000 (20:03 +0000)
commitfd52068e75c3ea1e67b2066ac9f7e2a862148a18
tree0dea1daaeeba01506ca94d3578d1c7963773b162tree | snapshot
parentd1bda83989a8c07395ec6818a0907f73252bd61ecommit | diff
Work in Progress: Who needs binary_morphisms? Curryfication is your friend.

But...

 1) the hints are uglier
 2) you really need to apply mk_binary_morphism to prove a curryfied binary
    morphism if you want to remain sane...

Note: with non uniform coercions everywhere we should be able to finally get
a beautiful script. Yet to be done.
helm/software/matita/nlibrary/logic/cprop.ma diff | blob | history
helm/software/matita/nlibrary/sets/setoids.ma diff | blob | history
helm/software/matita/nlibrary/sets/setoids1.ma diff | blob | history
helm/software/matita/nlibrary/sets/sets.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.