]> matita.cs.unibo.it Git - helm.git/commit
update in delayed_updating
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 30 May 2022 21:50:58 +0000 (23:50 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 30 May 2022 21:50:58 +0000 (23:50 +0200)
commitf5fa6554c93bec72a5bb098c0a2991fe294883b6
treec10ab63e2a0c107d66620174bfec5fba53710a45
parent12d58352dbd62df65d44becc0f69fc5a7b370866
update in delayed_updating

+ lift: additions and refactoring
+ reduction: WIP
15 files changed:
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_after.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_id.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_proper.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_uni.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_proper.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma [deleted file]