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=8fc0b30f2c359c68869d885584168a30d8b42028;hb=58ede527a29e92f47321820421a3d8d0735daad8;hp=1800e235000692e497566a29c0be878b0e40a519;hpb=e0f7a5025addf275e40372da3a39b0adacc8106f;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 1800e2350..8fc0b30f2 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 @@ -73,9 +73,9 @@ table { ] *) [ { "context-sensitive parallel r-computation" * } { - [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_length" + "lprs_drops" (* + "lprs_cprs" + "lprs_lprs" *) * ] + [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" (* + "lprs_cprs" + "lprs_lprs" *) * ] [ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ] - [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_drops" (* + "cprs_cprs" *) * ] + [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_lpr" (* + "cprs_cprs" *) * ] } ] [ { "t-bound context-sensitive parallel rt-computation" * } {