]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 24f99e7) | patch
Full specification of find. Added notation for If_Then_Else. Probably a delta
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 8 Sep 2007 17:21:58 +0000 (17:21 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 8 Sep 2007 17:21:58 +0000 (17:21 +0000)
commit35525e5acd7854210e2a1bbba07a4909117029ac
tree87c2f66abbe7cd43d37deb63d69f199d757e192atree | snapshot
parent24f99e747a9bfea3df90227e4b98082e4ad4dcaecommit | diff
Full specification of find. Added notation for If_Then_Else. Probably a delta
on t in the match the decides if it is the case to pass a coercion under a
match whould be nice.
matita/tests/coercions_russell.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.