Summary of the Specification
+ Summary of the Specification
Here is a numerical acount of the specification's contents
and its timeline.
+ Nodes are counted according to the "intrinsinc complexity measure"
+ [F. Guidi: "Procedural Representation of CIC Proof Terms"
+ Journal of Automated Reasoning 44(1-2), Springer (February 2010),
+ pp. 53-78].
category | -objects | -+ | category | +objects | +
|
- + |
|
- + |
|
- + |
|
- + |
|
sizes | files | -5 | +4 | characters | -5613 | +2567 | nodes | -9846 | +3637 | ||||
propositions | theorems | -4 | +2 | lemmas | 1 | total | -5 | +3 | |||||
concepts | declared | 3 | defined | -10 | +9 | total | -13 | +12 |
Logical Structure of the Specification
+ 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.
@@ -130,37 +134,25 @@
- component | -plane | -files | -+ | component | +plane | +files | +
|
MLTT1 | -- | genv_primitive | -judgement | +functional | +reduction and type machine | +rtm | +rtm_step ( ? ⨠? ) |
functional | -reduction and type machine | -rtm | -rtm_step ( ? ⨠? ) | -||||
+ |
|
- unfold | -lift ( â[?,?] ? ) | -subst ( [?â?] ? ) | -|||
examples | -- | + | relocation | +lift ( â[?,?] ? ) |
|
@@ -169,7 +161,7 @@
Physical Structure of the Specification
+ Physical Structure of the Specification
The source files are grouped in directories,
one for each component.
@@ -199,6 +191,6 @@
Last update: Sun, 21 Apr 2013 17:53:32 +0200
+ Last update: Sun, 06 Jul 2014 20:28:30 +0200