[lambda_delta home]
cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)
[Spacer]
Contents of the Specification
This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below.
Summary of the Specification
Here is a numerical acount of the specification's contents and its timeline.
categoryobjects




sizesfiles5bytes13143

propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
Logical Structure of the Specification
The source files are grouped in planes and components according to the following table. Each component contains its own notation file. The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders).
componentplanefiles
MLTT1genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
Physical Structure of the Specification
The source files are grouped in directories, one for each component.
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-10-16T20:12:15+02:00