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=784332f15c893c4aa287420488c83d13a2ea53b1;hb=f38fd769279794d0ca73c8945eac30e8b42e59be;hp=4176396a0b38f03f87019622dedc351336d00146;hpb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;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 4176396a0..784332f15 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 @@ -12,7 +12,7 @@ table { class "wine" [ { "iterated dynamic typing" * } { [ { "context-sensitive iterated native type assignment" * } { - [ [ "for terms" ] "ntas" + "( ⦃?,?⦄ ⊢ ? :*[?,?,?] ? )" "ntas_nta" + "ntas_preserve" * ] + [ [ "for terms" ] "ntas" + "( ⦃?,?⦄ ⊢ ? :*[?,?,?] ? )" "ntas_cpcs" + "ntas_nta" + "ntas_nta_ind" + " ntas_ntas" + "ntas_preserve" * ] } ] } @@ -92,6 +92,10 @@ table { ] class "cyan" [ { "rt-transition" * } { + [ { "context-sensitive parallel t-transition" * } { + [ [ "for terms" ] "cpt" + "( ⦃?,?⦄ ⊢ ? ⬆[?,?] ? )" "cpt_drops" + "cpt_fqu" + "cpt_cpm" * ] + } + ] [ { "context-sensitive parallel r-transition" * } { [ [ "normal form for terms" ] "cnr ( ⦃?,?⦄ ⊢ ➡[?] 𝐍⦃?⦄ )" "cnr_simple" + "cnr_tdeq" + "cnr_drops" * ] [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ] @@ -192,7 +196,7 @@ class "italic" { 2 } } ] [ { "global env. slicing" * } { - [ [ "" ] "gget ( ⬇[?] ? ≘ ? )" "gget_gget" * ] + [ [ "" ] "gget ( ⇩[?] ? ≘ ? )" "gget_gget" * ] } ] [ { "context-sensitive ordinary rt-substitution" * } {