]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / web / ground_src.tbl
index a4c2883e4b37347c9e45a639f7cf4089fdbd120e..edc2157eb715230b1993d674ca5ae2c792dd442e 100644 (file)
@@ -24,9 +24,9 @@ table {
       [ { "finite relocation with pairs" * } {
           [ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
           [ "fr2_minus ( ? ▭ ? ≘ ? )" * ]
-          [ "fr2_append ( ?@@? )" * ]
+          [ "fr2_append ( ?;;? )" * ]
           [ "fr2_plus ( ?+? )" * ]
-          [ "fr2_map (  ) ( ❨?,?❩;? )" * ]
+          [ "fr2_map ( 𝐞 ) ( ❨?,?❩;? )" * ]
         }
       ]
       [ { "total relocation" * } {
@@ -130,8 +130,13 @@ table {
           [ "stream ( ? ⨮{?} ? )" * ]
         }
       ]
+      [ { "lists" * } {
+          [ "list_append ( ?⨁{?}? )" "list_rcons ( ?⨭{?}? )" * ]
+          [ "list_length ( |?| )" * ]
+          [ "list ( ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" * ]
+        }
+      ]
       [ { "" * } {
-          [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" "list_length ( |?| )" * ]
           [ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
           [ "ltc" "ltc_ctc" * ]
           [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]