X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=5df7981032ddcf2c04040f3ae692ac80142c7abe;hb=c07e9b0a3e65c28ca4154fec76a54a9a118fa7e1;hp=f8b26841b9a867cf97c08d3f755b289ee313772e;hpb=93188fa3cfab893427b17b8b2084719cd43fac9c;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index f8b26841b..5df798103 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -72,29 +72,29 @@ sizes files - 5 + 4 characters - 5790 + 3928 nodes - 9846 + 3637 propositions theorems - 4 + 2 lemmas 1 total - 5 + 3 concepts declared 3 defined - 10 + 9 total - 13 + 12 @@ -138,29 +138,17 @@ - MLTT1 - - genv_primitive - judgement + functional + reduction and type machine + rtm + rtm_step ( ? ⇨ ? ) - functional - reduction and type machine - rtm - rtm_step ( ? ⇨ ? ) - - - +
- unfold - lift ( ↑[?,?] ? ) - subst ( [?←?] ? ) - - - examples - - + relocation + lift ( ↑[?,?] ? )
@@ -199,6 +187,6 @@

-
Last update: Thu, 16 May 2013 16:37:26 +0200
+
Last update: Sun, 21 Jul 2013 00:11:48 +0200