]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambda_delta/web/home/ld_basic_2.tbl
Basic_2 file names update
[helm.git] / helm / www / lambda_delta / web / home / ld_basic_2.tbl
index 0d05181402fa637c4cc6f65785a064ca51c28900..78d7b82373f4261d6610b5cd18f69ca7067f3382 100644 (file)
@@ -11,77 +11,89 @@ table {
    ]
    class "blue"
    [ { "examples" * } {
-         [ { "" * } {
-             [ "" * ]
-          }
-         ]
-      }
+        [ { "" * } {
+            [ "" * ]
+         }
+        ]
+     }
    ]
    class "sky"
    [ { "native typing" * } {
-         [ { "" * } {
-             [ "nty" * ]
-          }
-         ]
-      }
+        [ { "" * } {
+            [ "nty" * ]
+         }
+        ]
+     }
    ]
    class "cyan"
    [ { "conversion" * } {
-         [ { "context-sensitive" * } {
-             [ "cpcs" * ]
-          }
-         ]
-      }
+        [ { "context-sensitive conversion" * } {
+            [ "cpcs" * ]
+         }
+        ]
+     }
    ]
    class "water"
    [ { "computation" * } {
-         [ { "strongly normalizing" * } {
-             [ "csn" * ]
-          }
-         ]
-         [ { "context-sensitive" * } {
-             [ "cprs" * ]
-          }
-         ]
-      }
+        [ { "strongly normalizing computation" * } {
+            [ "csn" * ]
+         }
+        ]
+        [ { "context-sensitive computation" * } {
+            [ "cprs" * ]
+         }
+        ]
+     }
    ]
    class "green"
    [ { "reducibility" * } {
-         [ { "context-sensitive reduction" * } {
-             [ "lcpr" * ]
-             [ "cpr" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ]
-          }
-         ]
-         [ { "context-free normal forms" * } {
-             [ "tnf" * ]
-           }
-        ]
-         [ { "context-free reduction" * } {
-             [ "ltpr" "ltpr_ldrop" * ]
-             [ "tpr"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
-           }
-        ]
-         [ { "context-free reducible forms" * } {
-             [ "trf" * ]
-           }
-        ]
-      }
+        [ { "context-sensitive reduction" * } {
+            [ "lcpr" * ]
+            [ "cpr" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ]
+         }
+        ]
+        [ { "context-free normal forms" * } {
+            [ "twhnf" "tnf" * ]
+          }
+       ]
+        [ { "context-free reduction" * } {
+            [ "ltpr" "ltpr_ldrop" * ]
+            [ "tpr"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
+          }
+       ]
+        [ { "context-free reducible forms" * } {
+            [ "trf" * ]
+          }
+       ]
+        [ { "support for abstract reduction" * } {
+            [ "apr" "apr_cr" * ]
+          }
+       ]
+     }
    ]
    class "grass"
    [ { "static typing" * } {
-         [ { "atomic arity ass." * } {
-             [ "aaa" "aaa_lift" "aaa_aaa" * ]
-          }
-         ]
-         [ { "static type ass." * } {
-             [ "sty" "sty_lift" "sty_sty" * ]
-           }
-        ]
-      }
-   ]   
+        [ { "static type ass." * } {
+            [ "sty" "sty_lift" "sty_sty" * ]
+          }
+       ]
+        [ { "atomic arity ass." * } {
+            [ "aaa" "aaa_lift" "aaa_aaa" * ]
+         }
+        ]
+        [ { "parameters" * } {
+             [ "sh" * ]
+          }
+        ]
+     }
+   ]
    class "yellow"
    [ { "unfold" * } {
-        [ { "partial" * } {
+        [ { "term inverse relocation" * } {
+            [ "delift" * ]
+          }
+       ]
+       [ { "partial unfold" * } {
              [ "ltpss" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] 
             [ "tpss" "tpss_lift" "tpss_tpss" "tpss_ltps" * ]
           }
@@ -90,7 +102,7 @@ table {
    ]
    class "orange"   
    [ { "substitution" * } { 
-        [ { "parallel" * } {
+        [ { "parallel substitution" * } {
              [ "ltps" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ]
             [ "tps" "tps_lift" "tps_tps" * ]
           }
@@ -129,10 +141,6 @@ table {
              [ "aarity" * ]
          }
        ] 
-        [ { "parameters" * } {
-             [ "sh" * ]
-          }
-        ]
      }
    ]
 }