]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 754f746) | patch
1. For smart application, we only perforate small terms (terms with sort
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 4 Mar 2010 08:06:43 +0000 (08:06 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 4 Mar 2010 08:06:43 +0000 (08:06 +0000)
commitb879541d6103c346cfe14db79ff54249830a20fa
tree15395116defb9e2e9112128c542876ea7947cc78tree | snapshot
parent754f74638de5c287c849dc72494143b1da82cd88commit | diff
1. For smart application, we only perforate small terms (terms with sort
Type0). E.g. Not(P(a)) is perforated to Not(P(?)) and not to Not(?) as
before.
2. At maxdepth, we restrict the analysis to facts only in case the goal
is not reducible to a Pi. Example: if Not A = A -> False, Not A is not a
fact, and the previous politics would prune its application.
helm/software/components/ng_tactics/nnAuto.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.