cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
Summary of the Specification
Here is a numerical account of the specification's contents
and its timeline.
category |
objects |
|
|
|
|
|
sizes |
files |
39 |
characters |
59130 |
nodes |
107813 |
propositions |
theorems |
9 |
lemmas |
238 |
total |
247 |
concepts |
declared |
45 |
defined |
28 |
total |
73 |
-
2015 October 11.
Multiple relocation with lists of booleans.
-
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 |
|
|
|
|
|
multiple relocation |
|
trace ( ∥?∥ ) |
trace_at ( @⦃?,?⦄ ≡ ? ) |
trace_after ( ? ⊚ ? ≡ ? ) |
trace_isid ( 𝐈⦃?⦄ ) |
trace_sor ( ? ⋓ ? ≡ ? ) |
|
|
|
mr2 |
mr2_at ( @⦃?,?⦄ ≡ ? ) |
mr2_plus ( ? + ? ) |
mr2_minus ( ? ▭ ? ≡ ? ) |
|
|
natural numbers with infinity |
|
ynat ( ∞ ) |
ynat_pred ( ⫰? ) |
ynat_succ ( ⫯? ) |
ynat_le ( ? ≤ ? ) |
ynat_lt ( ? < ? ) |
ynat_plus ( ? + ? ) |
extensions to the library |
|
star |
lstar |
bool ( Ⓕ ) ( Ⓣ ) |
arith ( ?^? ) ( ⫯? ) ( ⫰? ) |
list ( ◊ ) ( ? @ ? ) ( |?| ) |
list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) |
generated logical decomposables |
|
xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ ) |
xoa_props ( ⊥ ) ( ⊤ ) |
|
|
|
|
|
|
|
|
|
|
|
|
Last update: Wed, 14 Oct 2015 21:43:44 +0200