X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2_src.tbl;h=7c16cd346c68ea4ac29d779bcd717fdbade5220c;hb=86a84e4116a8d388cb540bae6c60700f84a8f9f8;hp=b14263c1d428fa52862db2bd46037d4c3893400f;hpb=472cb969d9a01a6d24eabc39ba20d1dc6adf1b04;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index b14263c1d..7c16cd346 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -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" * } {