]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
- work in progress proceeds for the new definition of voids ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index 4368142cb476779fc4b97d676daa16d1559d7eb5..0dd04cb2cc7f415862dd4cf324671f220b7eb7ac 100644 (file)
@@ -238,6 +238,11 @@ table {
    ]
    class "red"
    [ { "syntax" * } {
+        [ { "equivalence up to exclusion binders" * } {
+             [ [ "" ] "voids ( ⓧ*[?]? ≋ ⓧ*[?]? )" "voids_length" + "voids_voids" * ]
+          }
+        ]
+   
         [ { "append for local environments" * } {
              [ [ "" ] "append ( ? @@ ? )" "append_length" * ]
           }
@@ -263,7 +268,6 @@ table {
         [ { "local environments" * } {
              [ [ "" ] "ceq_ext" "ceq_ext_ceq_ext" * ]
              [ [ "" ] "cext2" * ]
-             [ [ "" ] "lenv_voids ( ⓧ*[?]? )" * ]
              [ [ "" ] "lenv_length ( |?| )" * ]
              [ [ "" ] "lenv_weight ( ♯{?} )" * ]
              [ [ "" ] "lenv" * ]