]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6e17d96) | patch
The kernel _must_ check the correctness of the height since the reduction
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 5 Jun 2009 08:56:17 +0000 (08:56 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 5 Jun 2009 08:56:17 +0000 (08:56 +0000)
commit156b87c397a8b5cf9b7381def41e070e235941ee
treef7f28f26b2b621626742642771fd3f167b037b2dtree | snapshot
parent6e17d968f26fe09938c3e825ee9e9a431e244350commit | diff
The kernel _must_ check the correctness of the height since the reduction
machine never tries to reduce terms whose height is 0. Thus, if the
declared height is 0, the height is no longer an optimization!
helm/software/components/grafite_engine/grafiteEngine.ml diff | blob | history
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
helm/software/components/ng_kernel/nCicTypeChecker.mli diff | blob | history
helm/software/components/ng_kernel/nCicUntrusted.ml diff | blob | history
helm/software/components/ng_kernel/nCicUntrusted.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.