\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. Martin-Löf's Type Theory with one universe using λδ as theory of expressions.

Summary of the Specification $\lambda\delta butterfly$

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

2011 December 20. The Functional component is started inside the specification of λδ version 2.

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

$\lambda\delta rainbow rule$

Last update: Thu, 09 Mar 2017 13:38:17 +0100