X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fweb%2Fstatic_2_src.tbl;h=bce1a43764083a67932fea42a531b6335d490fd5;hp=f7afe7a1a95d195c57a356c0f45bcdace55c84a4;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index f7afe7a1a..bce1a4376 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -76,7 +76,7 @@ table { class "orange" [ { "relocation" * } { [ { "generic and uniform slicing" * } { - [ [ "for lenvs" ] "drops" + "( ⇩*[?,?] ? ≘ ? )" + "( ⇩*[?] ? ≘ ? )" "drops_ctc" + "drops_ltc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_sex" + "drops_lex" + "drops_seq" + "drops_drops" + "drops_vector" * ] + [ [ "for lenvs" ] "drops" + "( ⇩*[?,?] ? ≘ ? )" + "( ⇩[?] ? ≘ ? )" "drops_ctc" + "drops_ltc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_sex" + "drops_lex" + "drops_seq" + "drops_drops" + "drops_vector" * ] } ] [ { "basic relocation" * } { @@ -84,9 +84,9 @@ table { } ] [ { "generic and uniform relocation" * } { - [ [ "for binders" ] "lifts_bind" + "( ⇧*[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] - [ [ "for term vectors" ] "lifts_vector" + "( ⇧*[?] ? ≘ ? )" "lifts_lifts_vector" * ] - [ [ "for terms" ] "lifts" + "( ⇧*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_teqx" + "lifts_tweq" + "lifts_teqo" + "lifts_lifts" * ] + [ [ "for binders" ] "lifts_bind" + "( ⇧*[?] ? ≘ ? )" + "( ⇧[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] + [ [ "for term vectors" ] "lifts_vector" + "( ⇧*[?] ? ≘ ? )" + "( ⇧[?] ? ≘ ? )" "lifts_lifts_vector" * ] + [ [ "for terms" ] "lifts" + "( ⇧*[?] ? ≘ ? )" + "( ⇧[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_teqx" + "lifts_tweq" + "lifts_teqo" + "lifts_lifts" * ] } ] [ { "syntactic equivalence" * } {