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