X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=5ae7da3063e1448a8bed8e391e332259463afc03;hb=ecb63d645415784352a937f8320f84c23da327f7;hp=4003948a122714eaebe56cba462424f74d8ba675;hpb=93bba1c94779e83184d111cd077d4167e42a74aa;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 4003948a1..5ae7da306 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -144,29 +144,29 @@
sizes |
files |
- 83 |
+ 102 |
characters |
- 55955 |
+ 69295 |
nodes |
- 191279 |
+ 245853 |
propositions |
theorems |
- 33 |
+ 34 |
lemmas |
- 211 |
+ 256 |
total |
- 244 |
+ 290 |
concepts |
declared |
- 15 |
+ 21 |
defined |
- 23 |
+ 29 |
total |
- 38 |
+ 50 |
@@ -343,40 +343,80 @@
- relocation |
- ranged equivalence for closures |
- freq ( �,?,?⦠⡠�,?,?⦠) |
- freq_freq |
-
+ | static typing |
+ parameters |
+ sh |
+ sd |
+
|
-
+ |
|
-
+ |
|
- context-sensitive free variables |
- frees ( ? ⢠ð
*�⦠⡠? ) |
- frees_weight frees_lreq frees_frees |
-
+ | restricted ref. for local env. |
+ lsubr ( ? â« ? ) |
+ lsubr_length lsubr_drops lsubr_lsubr |
+
|
-
+ |
|
-
+ |
|
- generic slicing for local environments |
- drops_vector ( â¬*[?,?] ? â¡ ? ) |
-
+ | ranged equivalence for closures |
+ freq ( �,?,?⦠⡠�,?,?⦠) |
+ freq_freq |
+
|
+
+
+ |
+
+
+
+
+ |
+ context-sensitive free variables |
+ frees ( ? ⢠ð
*�⦠⡠? ) |
+ frees_weight frees_lreq frees_frees |
+
+
+ |
+
+
+ |
+
+
+ s-computation |
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ s-transition |
+ structural successor for closures |
+ fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq_length fquq_weight |
|
@@ -391,8 +431,8 @@
|
- drops ( â¬*[?,?] ? â¡ ? ) |
- drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
+ fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fqu_length fqu_weight |
|
@@ -401,72 +441,86 @@
-
+ | relocation |
+ generic slicing for local environments |
+ drops_vector ( â¬*[?,?] ? â¡ ? ) |
+
|
- generic relocation for terms |
- lifts_vector ( â¬*[?] ? â¡ ? ) |
- lifts_lift_vector |
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
- lifts ( â¬*[?] ? â¡ ? ) |
- lifts_simple lifts_weight lifts_lifts |
-
+ | drops ( â¬*[?,?] ? â¡ ? ) |
+ drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
+
|
-
+ |
|
-
+ |
|
- ranged equivalence for local environments |
- lreq ( ? â¡[?] ? ) |
- lreq_length lreq_lreq |
-
+ | generic relocation for terms |
+ lifts_vector ( â¬*[?] ? â¡ ? ) |
+ lifts_lifts_vector |
+
|
-
+ |
|
-
+ |
|
- generic entrywise extension of context-sensitive relations for terma |
- lexs ( ? ⦻*[?,?,?] ? ) |
- lexs_length lexs_lexs |
-
+ |
|
-
+ | lifts ( â¬*[?] ? â¡ ? ) |
+ lifts_simple lifts_weight lifts_lifts |
+
+
+ |
+
|
- |
- |
-
+ |
|
+ ranged equivalence for local environments |
+ lreq ( ? â¡[?] ? ) |
+ lreq_length lreq_lreq |
|
+
+
+ |
+
+
+
+
+ |
+ generic entrywise extension of context-sensitive relations for terma |
+ lexs ( ? ⦻*[?,?,?] ? ) |
+ lexs_length lexs_lexs |
|
@@ -476,6 +530,20 @@
grammar |
+ append for local environments |
+ append ( ? @@ ? ) |
+ append_length |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
context-sensitive equivalences for terms |
ceq |
ceq_ceq |
@@ -540,7 +608,9 @@
lenv |
lenv_weight ( â¯{?} ) |
lenv_length ( |?| ) |
- lenv_append ( ? @@ ? ) |
+
+
+ |
@@ -617,6 +687,6 @@
- Last update: Sun, 27 Mar 2016 18:42:29 +0200
+ Last update: Fri, 01 Apr 2016 23:30:53 +0200
|