]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f951f6a) | patch
New strategy for let-in unfolding (aka zeta reduction): a reference to a
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Sep 2005 14:27:39 +0000 (14:27 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Sep 2005 14:27:39 +0000 (14:27 +0000)
commit13f7f0dcaa42805d33003850a0eb94d1c277fddd
treea043dc2a83b118b8b0925baafe9cc76021d3c548tree | snapshot
parentf951f6a1c14f33b624789bcf60e80d8307b461d3commit | diff
New strategy for let-in unfolding (aka zeta reduction): a reference to a
let-bound variable is expanded if and only if the simplified form of its definiendum (applied to the actual arguments) is different from the
non-simplified form.
helm/ocaml/tactics/proofEngineReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.