X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_1.html;h=739454623d63d475385335801e071c8b01ee6639;hb=e36a0eced135e6f1b79d06c78a408918f65376b6;hp=0b8626498731c56ab9eae528ecdefbebefad802f;hpb=a3ab07c97eaea90a6f243f2053fb55151ecc12df;p=helm.git diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 0b8626498..739454623 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -102,18 +102,68 @@ - +

Abstract Syntax and Behavior [spacer]

This is a summary of available syntactic items and reductions (block structure). +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

domain	block	leader	âÎ¶ *	annotator (with âÏµ *)	applicator (with âÎ¸ *)	reference *	reduction
{X \| Î â¢ â¤}	exclusion	Î â¢ Ï	yes	no	no	no	no
{X \| Î â¢ X : W}	typed abstraction	Î â¢ Î»W	no	<W>	(V)	#i	âÎ² *
{X \| Î â¢ X = V}	abbreviation	Î â¢ Î´V	yes	no	no	#i	âÎ´
no	sort	Î â¢ âk	no	no	no	no	no

* In terms only. +

Summary of the Specification [spacer]

Here is a numerical account of the specification's contents @@ -146,18 +196,18 @@ files 120 characters - 198123 + 198089 nodes propositions theorems - 699 + 81 lemmas - 29 + 618 total - 728 + 699 concepts @@ -773,6 +823,6 @@

Last update: Mon, 19 Jan 2015 23:52:52 +0100

Last update: Thu, 05 Mar 2015 16:42:28 +0100