]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dc35589) | patch
1) Notation for dependent pairs differentiated from that for sigma types.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 14 Dec 2011 12:18:07 +0000 (12:18 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 14 Dec 2011 12:18:07 +0000 (12:18 +0000)
commitc9c6cae5121a25b05450ea42578f14f74569cfbf
tree54c5a1a261c4250948c81cefed0e75d70c16f75btree | snapshot
parentdc35589f8448d6a7bd803992e918acc7b720e7fbcommit | diff
1) Notation for dependent pairs differentiated from that for sigma types.
2) Russell now works directly on mk_Sig/pi1
matita/matita/lib/basics/core_notation.ma diff | blob | history
matita/matita/lib/basics/russell.ma diff | blob | history
matita/matita/lib/basics/types.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.