+
+
+
-
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=8a22ab925ea6424271c18a604faef968a40e1379;hb=5a81feec7b8c07a43e96d772431e06bad177ed8c;hp=e5218996f8e362497548f1df7f8acb5b337263e0;hpb=7562d9781dc4f351ddc3b2f8edd21f4976621948;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index e5218996f..8a22ab925 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -16,14 +16,14 @@
sizes | files | -30 | +102 | characters | -68581 | +143239 | nodes | -62380 | +332314 |
propositions | theorems | -2 | +42 | lemmas | -187 | +679 | total | -189 | +721 |
concepts | declared | -40 | +65 | defined | -25 | +70 | total | -65 | +135 |
|
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
|
||||||||||||||||||
natural numbers with infinity | +generic rt-transition counter | ++ | rtc ( â©?,?,?,?⪠) ( ðð ) ( ðð ) ( ðð ) | +rtc_isrc ( ððâ¦?, ?⦠) | +rtc_shift ( â? ) | +rtc_max ( ? ⨠? ) | +rtc_plus ( ? + ? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ ||||||||
multiple relocation | ++ | rtmap | +rtmap_eq ( ? â ? ) | +rtmap_pushs ( â*[?]? ) | +rtmap_nexts ( ⫯*[?]? ) | +rtmap_tl ( ⫱? ) | +rtmap_tls ( ⫱*[?]? ) | +rtmap_isid ( ðâ¦?⦠) | +rtmap_id | +rtmap_isdiv ( ðâ¦?⦠) | +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_sor | ++ | 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 ( â*[?]? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
extensions to the library | +
+ + |
+
+ + |
+ list ( â ) ( ? @ ? ) ( |?| ) | +list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ ||||||||
+ + |
+
+ + |
+ bool ( â» ) ( â ) | +arith ( ?^? ) ( ⫯? ) ( â«°? ) ( ? ⨠? ) ( ? ⧠? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ |||||||||
+ + |
+
+ + |
+ relations | +star | +lstar | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ |||||||||
generated logical decomposables | - | star | -lstar | -bool ( â» ) ( â ) | -arith ( ?^? ) | -list ( â ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) | +xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) | +xoa_props ( ⥠) ( ⤠) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
|
@@ -232,10 +789,47 @@
|||||||
generated logical decomposables | +- | xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) | -xoa_props ( ⥠) ( ⤠) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
|
@@ -261,9 +855,8 @@