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

This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below.

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

category	objects
sizes	files	14	characters	6787	nodes	10070
propositions	theorems	2	lemmas	4	total	6
concepts	declared	6	defined	11	total	17

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

component	plane	files
functional	reduction and type machine	rtm	rtm_step ( ? ⇨ ? )
	relocation	lift ( ↑[?,?] ? )