]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
update in basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index e719304bfa322f3fdaab9c9a5c43676e208a27a0..3fe0cbccb8605c0295d6d07cbbb7524ffe6335d4 100644 (file)
@@ -12,7 +12,7 @@ table {
    class "wine"
    [ { "iterated dynamic typing" * } {
         [ { "context-sensitive iterated native type assignment" * } {
-             [ [ "for terms" ] "ntas" + "( ⦃?,?⦄ ⊢ ? :*[?,?,?] ? )" "ntas_nta" + "ntas_preserve" * ]
+             [ [ "for terms" ] "ntas" + "( ⦃?,?⦄ ⊢ ? :*[?,?,?] ? )" "ntas_cpcs" + "ntas_nta" + "ntas_nta_ind" + " ntas_ntas" + "ntas_preserve" * ]
           }
         ]
      }
@@ -25,7 +25,7 @@ table {
         ]
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
           }
         ]
      }