X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=684cefd20c2e23e8a2ff6017100462e015697272;hb=5e5f9111df82a2f84f2b560ab59392cf0e0906c0;hp=d3b26812c83c65f748cabfd9ec3e6a5cbd48c383;hpb=1e89c373698e2b5e55661291f25dc5238e9f13fd;p=helm.git
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index d3b26812c..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: Sat, 21 Jan 2017 15:35:26 +0100
+ Last update: Sat, 01 Apr 2017 16:50:39 +0200