cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
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 |
|
|
|
|
|
sizes |
files |
29 |
characters |
72188 |
nodes |
57742 |
propositions |
theorems |
2 |
lemmas |
171 |
total |
173 |
concepts |
declared |
40 |
defined |
24 |
total |
64 |
-
2013 November 27.
Natural numbers with infinity.
-
2011 August 10.
Specification starts.
Logical Structure of the Specification
The source files are grouped in planes
according to the following table.
Notation files covering the whole specification are provided.
The notation for the relations or functions introduced in each file
is shown in parentheses (? are placeholders).
plane |
files |
|
|
|
|
|
|
|
|
natural numbers with infinity |
ynat ( ∞ ) |
ynat_pred ( ⫰? ) |
ynat_succ ( ⫯? ) |
ynat_le ( ?≤? ) |
ynat_lt ( ?<? ) |
ynat_minus ( ? - ? ) |
ynat_plus ( ? + ? ) |
ynat_max |
ynat_min |
extensions to the library |
arith.ma ( ?^? ) |
|
|
|
|
|
|
|
|
generated logical decomposables |
xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ ) |
xoa_props ( ⊥ ) ( ⊤ ) |
|
|
|
|
|
|
|
Physical Structure of the Specification
The source files are grouped in directories,
one for each plane.
Last update: Sat, 22 Feb 2014 12:36:18 +0100