]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
commit completed! the new iterated static type assignment is up!
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index b14263c1d428fa52862db2bd46037d4c3893400f..7c16cd346c68ea4ac29d779bcd717fdbade5220c 100644 (file)
@@ -51,7 +51,7 @@ table {
           }
         ]
         [ { "stratified native validity" * } {
-             [ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" "shnv_aaa" * ]
+             [ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
              [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_scpes" + "snv_preserve" * ]
           }
         ]
@@ -178,7 +178,7 @@ table {
           }
         ]
         [ { "iterated static type assignment" * } {
-             [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? )" "lstas_lift" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
+             [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
           }
         ]
      }
@@ -190,11 +190,7 @@ table {
           }
         ]
         [ { "degree assignment" * } {
-             [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_sta" + "da_da" * ]
-          }
-        ]
-        [ { "static type assignment" * } {
-             [ "sta ( ⦃?,?⦄ ⊢ ? •[?] ? )" "sta_lift" + "sta_lpx_sn" + "sta_aaa" + "sta_sta" * ]
+             [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_da" * ]
           }
         ]
         [ { "parameters" * } {