+
+
+
-
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=1a9b9352fa83780b81626d8fec8e83f4412b44ee;hb=282936907bd9b37d9de37f14e0e497db16f5d8b0;hp=669d0f08fa781e03728001191dae5b3e67ef0ad8;hpb=25577a78cccba09974c91fcbfea770091a413382;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 669d0f08f..1a9b9352f 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -16,14 +16,14 @@
sizes | files | -30 | +92 | characters | -68581 | +125262 | nodes | -62380 | +265747 |
propositions | theorems | -2 | +33 | lemmas | -187 | +588 | total | -189 | +621 |
concepts | declared | -40 | +60 | defined | -25 | +63 | total | -65 | +123 |
|
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
|
||||||||||||||||||
natural numbers with infinity | +generic rt-transition counter | ++ | rtc ( â©?,?,?,?⪠) ( ðð ) ( ðð ) ( ðð ) | +rtc_isrc ( ððâ¦?, ?⦠) | +rtc_shift ( â? ) | +rtc_plus ( ? + ? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ ||||||||
multiple relocation | ++ | rtmap | +rtmap_eq ( ? â ? ) | +rtmap_pushs ( â*[?]? ) | +rtmap_tl ( ⫱? ) | +rtmap_tls ( ⫱*[?]? ) | +rtmap_isid ( ðâ¦?⦠) | +rtmap_id | +rtmap_fcla ( ðâ¦?⦠⡠? ) | +rtmap_isfin ( ð â¦?⦠) | +rtmap_isuni ( ðâ¦?⦠) | +rtmap_uni ( ðâ´?âµ ) | +rtmap_sle ( ? â ? ) | +rtmap_sand ( ? â ? â¡ ? ) | +rtmap_sor ( ? â ? â¡ ? ) | +rtmap_at ( @â¦?,?⦠⡠? ) | +rtmap_istot ( ðâ¦?⦠) | +rtmap_after ( ? â ? â¡ ? ) | +rtmap_coafter ( ? ~â ? â¡ ? ) | +|||||||||
+ + |
+
+ + |
+ nstream ( â? ) ( ⫯? ) | +nstream_eq | ++ | + | + | nstream_isid | +nstream_id ( ðð ) | ++ | + | + | + | + | nstream_sand | ++ | + | nstream_istot ( ?@â´?âµ ) | +nstream_after ( ? â ? ) | +nstream_coafter ( ? ~â ? ) | +|||||||||
+ + |
+
+ + |
+ mr2 | +mr2_at ( @â¦?,?⦠⡠? ) | +mr2_plus ( ? + ? ) | +mr2_minus ( ? â ? â¡ ? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ |||||||||
natural numbers with infinity | ++ | ynat ( â ) | +ynat_pred ( â«°? ) | +ynat_succ ( ⫯? ) | +ynat_le ( ? ⤠? ) | +ynat_lt ( ? < ? ) | +ynat_plus ( ? + ? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ |||||||||
extensions to the library | - | ynat ( â ) | -ynat_pred ( â«°? ) | -ynat_succ ( ⫯? ) | -ynat_le ( ? ⤠? ) | -ynat_lt ( ? < ? ) | -ynat_minus ( ? - ? ) | -ynat_plus ( ? + ? ) | -ynat_max | -ynat_min | +stream ( ? @ ? ) | +stream_eq ( ? â ? ) | +stream_hdtl ( â? ) | +stream_tls ( â*[?]? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ list ( â ) ( ? @ ? ) ( |?| ) | +list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ |||||||||
+ + |
+
+ + |
+ bool ( â» ) ( â ) | +arith ( ?^? ) ( ⫯? ) ( â«°? ) ( ? ⨠? ) ( ? ⧠? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ |||||||||
+ + |
+
+ + |
+ star | +lstar | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
|||||||||
extensions to the library | +generated logical decomposables | - | star | -lstar | -bool ( â» ) ( â ) | -arith ( ?^? ) | -list ( â ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) | +xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) | +xoa_props ( ⥠) ( ⤠) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
|
@@ -232,10 +735,41 @@
||||||
generated logical decomposables | +- | xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) | -xoa_props ( ⥠) ( ⤠) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
|
@@ -261,9 +795,8 @@