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.
category |
objects |
|
|
|
|
|
sizes |
files |
30 |
characters |
68581 |
nodes |
62380 |
propositions |
theorems |
2 |
lemmas |
187 |
total |
189 |
concepts |
declared |
40 |
defined |
25 |
total |
65 |
-
2013 November 27.
Natural numbers with infinity.
-
2011 August 10.
Specification starts.
Logical Structure of the Specification
This table reports the specification's components and their planes.
component |
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 |
|
star |
lstar |
bool ( Ⓕ ) ( Ⓣ ) |
arith ( ?^? ) |
list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) |
|
|
|
|
generated logical decomposables |
|
xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ ) |
xoa_props ( ⊥ ) ( ⊤ ) |
|
|
|
|
|
|
|
Last update: Tue, 04 Nov 2014 16:28:52 +0100