]> matita.cs.unibo.it Git - helm.git/commitdiff
partial update in basic_2 ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 3 Sep 2012 14:32:06 +0000 (14:32 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 3 Sep 2012 14:32:06 +0000 (14:32 +0000)
helm/www/lambda_delta/web/home/basic_2_src.tbl

index 698c8b1fafafa2469d75e691689f90bf5021c206..2252411ce6f700f0048a3777891de13716bee674 100644 (file)
@@ -117,6 +117,11 @@ table {
              [ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ]
           }
         ]
+        [ { "focalized reduction" * } {
+             [ "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" * ]
+             [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" * ]
+          }
+        ]
         [ { "context-free normal forms" * } {
              [ "thnf ( 𝐇𝐍⦃?⦄ )"   * ]
           }
@@ -211,7 +216,7 @@ table {
           }
         ]
         [ { "local env. ref. for substitution" * } {
-             [ "lsubs ( ? ≼[?,?] ? )" "lsubs_lsubs" "lsubs_sfr ( ≽[?,?] ? )" * ]
+             [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ]
           }
         ]
         [ { "basic term relocation" * } {
@@ -224,7 +229,7 @@ table {
    class "red"   
    [ { "grammar" * } {
         [ { "same head term form" * } {
-             [ "tshf ( ? ≈ ? )" "tshf_tshf" * ]
+             [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ]
           }
         ]
         [ { "same top term constructor" * } {
@@ -237,7 +242,7 @@ table {
         ]
         [ { "internal syntax" * } {
              [ "genv" * ]
-             [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" * ]
+             [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" "lenv_px_bi" * ]
              [ "term" "term_weight ( #{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
              [ "item" * ]
           }