]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ff57c60) | 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)
commite464d2ad85f2a3902f911e28f06a54b7fa16d2d7
tree1580b56db47ba70e706eaa56bdb4b24d207572a8tree | snapshot
parentff57c6060afde70bec70bc620ae17f88d9e985e4commit | 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.
helm/software/matita/tests/dependent_type_inference.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.