]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6db1265) | patch
Yet another strategy for let...ins: a let-in is _NEVER_ simplified.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Jan 2006 17:59:43 +0000 (17:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Jan 2006 17:59:43 +0000 (17:59 +0000)
commit812e565e94b0e926c48614127d0672c4e04e2ce7
treece0a376c463fa18d9e4a514fb216e0f95d8c351etree | snapshot
parent6db12650bceb071d9b5ea8f882613a98bd6df79bcommit | diff
Yet another strategy for let...ins: a let-in is _NEVER_ simplified.
The user has to use unfold to zeta-expand it.
(Thus, a let-in is more opaque than a constant in the environment.)
helm/matita/tests/simpl.ma diff | blob | history
helm/ocaml/tactics/proofEngineReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.