]> matita.cs.unibo.it Git - helm.git/commit
update in delayed_updating
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 24 Jan 2022 23:30:11 +0000 (00:30 +0100)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 24 Jan 2022 23:30:11 +0000 (00:30 +0100)
commit80ecd5486c6013f6c297173f41432fd1d93814ef
tree47452e2d06f33f485603881b1b702646e3408e63
parent8d8863982ca95225551e9659ed431db046c34e81
update in delayed_updating

+ bugs fixed in depth, dfr, ifr
+ WIP on dfr_lift_bi
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure_depth.ma
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma