]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 85fcff9) | patch
update in delayed-updating
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Thu, 3 Feb 2022 13:11:58 +0000 (14:11 +0100)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Thu, 3 Feb 2022 13:11:58 +0000 (14:11 +0100)
commitd43c110267c05246b638e7f944e065820d5c1197
tree878d9d54acab12aca28720833ca9f7d8165be947tree | snapshot
parent85fcff9664b400a1cf25f383505638ffe34222b6commit | diff
update in delayed-updating

+ relationship between updating an grafted terms clarified
+ progress with dfr-lift_bi
matita/matita/contribs/lambdadelta/delayed_updating/notes.txt diff | blob | history
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma diff | blob | history
matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm_eq.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma diff | blob | history
matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma diff | blob | history
matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma diff | blob | history
matita/matita/contribs/lambdadelta/ground/lib/list_append.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.