]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
- exclusion binder in local environments:
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index 059745fe9568a4bedfa5f3ef044f422db158b74e..0fd7f15f7ad5a565b87c80b7332e952b6f6de914 100644 (file)
@@ -123,8 +123,10 @@ table {
         ]
      }
    ]
+*)
    class "cyan"
    [ { "rt-transition" * } {
+(*
         [ { "uncounted rst-transition" * } {
              [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
              [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
@@ -136,9 +138,11 @@ table {
              [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ]
           }
         ]
+*)
         [ { "uncounted context-sensitive rt-transition" * } {
              [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
              [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ]
+             [ "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
              [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
           }
         ]
@@ -156,7 +160,6 @@ table {
         ]
      }
    ]
-*)
    class "green"
    [ { "static typing" * } {
         [ { "generic reducibility" * } {
@@ -241,8 +244,9 @@ table {
              [ "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
           }
         ]
-        [ { "degree-based equivalence for terms" * } {
-             [ "tdeq ( ? ≡[?,?] ? ) " "tdeq_ext" + "tdeq_tdeq" * ]
+        [ { "degree-based equivalence" * } {
+             [ "tdeq_ext ( ? ≡[?,?] ? )" * ]
+             [ "tdeq ( ? ≡[?,?] ? )" "tdeq_tdeq" * ]
           }
         ]
         [ { "closures" * } {