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=236b4f999d77e20a1d6af9ad3d6f0db9767366b9;hb=3c6ff3987c3cc5e2df03fb76d07697c28c89c0a8;hp=f02240094297af8b7e0cad9da7e600412b8f805b;hpb=084ea7868f6153effc18e8ee1c0e6cdb34d181c0;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 f02240094..236b4f999 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 @@ -20,7 +20,7 @@ table { class "magenta" [ { "dynamic typing" * } { [ { "context-sensitive native type assignment" * } { - [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_ind" * ] + [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" * ] } ] [ { "context-sensitive native validity" * } { @@ -40,6 +40,10 @@ table { ] class "blue" [ { "rt-conversion" * } { + [ { "context-sensitive parallel eta-conversion" * } { + [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ] + } + ] [ { "context-sensitive parallel r-conversion" * } { [ [ "for terms" ] "cpc" + "( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] }