From c038f0446312091a30179fd80e6ffd3ec39ab446 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 6 Jul 2022 14:18:48 +0200 Subject: [PATCH] partial commit in delayed_updating + parchin reverse operator for paths --- .../functions/nec_r_1.ma => etc/reverse/nec_r_1.etc} | 0 .../reverse/path_depth_reverse.etc} | 0 .../path_reverse.ma => etc/reverse/path_reverse.etc} | 0 .../reverse/path_structure_reverse.etc} | 0 .../contribs/lambdadelta/delayed_updating/names.txt | 9 +++++++++ 5 files changed, 9 insertions(+) rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/nec_r_1.ma => etc/reverse/nec_r_1.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{syntax/path_depth_reverse.ma => etc/reverse/path_depth_reverse.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{syntax/path_reverse.ma => etc/reverse/path_reverse.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{syntax/path_structure_reverse.ma => etc/reverse/path_structure_reverse.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/names.txt diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nec_r_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/nec_r_1.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nec_r_1.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/nec_r_1.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_reverse.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_depth_reverse.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_reverse.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_depth_reverse.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_reverse.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_reverse.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_reverse.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_reverse.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_reverse.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_structure_reverse.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_reverse.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_structure_reverse.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/names.txt b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt new file mode 100644 index 000000000..aee943494 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt @@ -0,0 +1,9 @@ +METAVARIABLES + + b : balanced path + f, g : update function + h, k : reference index by depth + l : label + m, n : natural number + p, q, r, s: path + t, u, v, w: term -- 2.39.2