\lambda\delta home page

X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=eb3ac6cda67486665bdc8d39be457a8286b3eb5e;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=e23bd8eddc540d4f33bb179b0f9efe600fb0d3ea;hpb=e866d78af74246133f5a14cb711a62af39308dee;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index e23bd8edd..eb3ac6cda 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -1,26 +1,261 @@ -\lambda\delta home page

$[\lambda\delta home]$

cic:/matita/lambdadelta/apps_2/ (applications of Î»Î´ version 2)

$\lambda\delta rainbow rule$

home	news	specification			documentation	implementation
foreword	milestones	version 2	(background - core - applications)		version 2	helena	Open Symbolic Notation (OSN)
citations	visibility	version 1	(background - core)	(static HELM directory)	version 1	library	(static LDDL directory)

Contents of the Specification $\lambda\delta butterfly$

This specification comprises a collection of checked + + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

cic:/matita/lambdadelta/apps_2/ (applications of Î»Î´ version 2)

+ $\lambda\delta rainbow rule$ +

+
+

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

+ home +	+ news +	+ specification +	+ +	+ +	+ documentation +	+ implementation +	+ +
+ foreword +	+ milestones +	+ version 2 +	(background - core - applications)	+ +	+ version 2 +	+ helena +	+ Open Symbolic Notation (OSN) +
+ citations +	+ visibility +	+ version 1 +	(background - core)	(static HELM directory)	+ version 1 +	+ library +	(static LDDL directory)

Contents of the Specification $\lambda\delta butterfly$ +

This specification comprises a collection of checked applications of Î»Î´ version 2. In particular it contains the components below. -

MLTT1. +

+ MLTT1. Martin-LÃ¶f's Type Theory with one universe using Î»Î´ as theory of expressions. -

Functional. +

+ Functional. The validation algorithm for Î»Î´ as implemented in Helena 0.8. -

Examples. +

+ Examples. Terms of Î»Î´ with special features. -

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents + + +

Summary of the Specification $\lambda\delta butterfly$ +

Here is a numerical account of the specification's contents and its timeline. -

category	objects
sizes	files	1	characters	377	nodes	775
propositions	theorems	2	lemmas	1	total	3
concepts	declared	0	defined	3	total	3

2017 March 6. +

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

category	units	+ +	+ +	+ +	+ +	+ +
sizes	characters (files)	377 (1)	nodes (objects)	779 (6)	intrinsic loss factor	2.1
propositions	theorems	2	lemmas	1	total	3
concepts	declared	0	defined	3	total	3

+ 2017 March 6. The Examples component is moved from the Core directory. -

2012 February 24. +

+ 2012 February 24. The Applications directory is started. -

2011 December 20. +

+ 2011 December 20. The Functional component is started inside the specification of Î»Î´ version 2. -

2011 December 12. +

+ 2011 December 12. The MLTT1 component is started. -

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes. -

component	plane	files
functional	reduction and type machine	rtm	rtm_step ( ? â¨ ? )
	relocation	lift ( â[?,?] ? )
examples	terms with special features	ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta