]> matita.cs.unibo.it Git - helm.git/commit
update in delayed_updating
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 27 Dec 2022 16:08:00 +0000 (17:08 +0100)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 27 Dec 2022 16:08:00 +0000 (17:08 +0100)
commitcf2a049a6cc888f6c5d0637ab0523f186058fc8f
tree5388703a74829a9426a8468fe92c2b34623f67e8
parentd89ef541a62a996a7e7fa4d4a1cfc3b28d7862e5
update in delayed_updating

+ more complex example in which discarding num labels in b solves unwind
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_zero.ma [deleted file]