]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4a1f42f) | patch
This test shows one of the few cases were Matita is able to infer a dependent
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Sep 2007 08:34:41 +0000 (08:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Sep 2007 08:34:41 +0000 (08:34 +0000)
commit81ca7521b39937cf79056465e18b4666ce1f34ff
tree060611e8cd734145c30edabe1a4c1565d8196ecdtree | snapshot
parent4a1f42f90d32e6839b453e15bb5aec0d816c60eacommit | diff
This test shows one of the few cases were Matita is able to infer a dependent
type. It should break if the dependent type is no longer inferred.
matita/tests/dependent_type_inference.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.