X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=684cefd20c2e23e8a2ff6017100462e015697272;hb=5e5f9111df82a2f84f2b560ab59392cf0e0906c0;hp=8c3fad8d70ee79df0ac57b3ce92a9ce6f5a74999;hpb=06531086fc492d0fd374ada30e116b56a5eff957;p=helm.git
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 8c3fad8d7..684cefd20 100644
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -120,6 +120,12 @@
Functional.
The validation algorithm for λδ as implemented in
Helena 0.8.
+
+
+
+ -
+ Examples.
+ Terms of λδ with special features.
Summary of the Specification
@@ -154,31 +160,37 @@
files |
1 |
characters |
-
217 |
+
377 |
nodes |
-
0 |
+
779 |
propositions |
theorems |
- 0 |
+ 2 |
lemmas |
- 0 |
+ 1 |
total |
- 0 |
+ 3 |
concepts |
declared |
0 |
defined |
- 0 |
+ 3 |
total |
- 0 |
+ 3 |
+
+ -
+ 2017 March 6.
+ The Examples component is moved from the Core directory.
+
+
-
2012 February 24.
@@ -214,17 +226,25 @@
- functional |
- reduction and type machine |
- rtm |
- rtm_step ( ? ⨠? ) |
+ functional |
+ reduction and type machine |
+ rtm |
+ rtm_step ( ? ⨠? ) |
-
+ |
+
+ |
+ relocation |
+ lift ( â[?,?] ? ) |
+
|
- relocation |
- lift ( â[?,?] ? ) |
+
+
+ examples |
+ terms with special features |
+ ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta |
|
@@ -258,6 +278,6 @@
- Last update: Sun, 05 Mar 2017 18:09:44 +0100
+ Last update: Sat, 01 Apr 2017 16:50:39 +0200