]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 00bb9e0) | 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)
commit48b5f69a87f0f4e067c89085ddd1ae503e53e068
treee3633483f598545051302abeba864072aaf81967tree | snapshot
parent00bb9e0e9e23b6d68e0d56bdeb96245673495a68commit | 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.
helm/software/matita/tests/coercions_russell.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.