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 |
69 |
characters |
83843 |
nodes |
168516 |
propositions |
theorems |
14 |
lemmas |
388 |
total |
402 |
concepts |
declared |
42 |
defined |
44 |
total |
86 |
-
2016 March 4.
Platform-independent multiple relocation (rtmap).
-
2016 January 20.
Multiple relocation with streams of naturals.
-
2015 October 11.
Multiple relocation with lists of booleans.
-
2013 November 27.
Natural numbers with infinity (ynat).
-
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_plus ( ? + ? ) |
|
|
|
|
|
multiple relocation |
|
rtmap |
rtmap_eq ( ? ≗ ? ) |
rtmap_tl ( ⫱? ) |
rtmap_tls ( ⫱*[?]? ) |
rtmap_isid ( 𝐈⦃?⦄ ) |
rtmap_id |
rtmap_sle ( ? ⊆ ? ) |
rtmap_sand ( ? ⋒ ? ≡ ? ) |
rtmap_at ( @⦃?,?⦄ ≡ ? ) |
rtmap_istot ( 𝐓⦃?⦄ ) |
rtmap_after ( ? ⊚ ? ≡ ? ) |
|
|
nstream ( ↑? ) ( ⫯? ) |
nstream_eq |
|
|
nstream_isid |
nstream_id ( 𝐈𝐝 ) |
|
nstream_sand |
|
nstream_istot ( ?@❴?❵ ) |
nstream_after ( ? ∘ ? ) |
|
|
mr2 |
mr2_at ( @⦃?,?⦄ ≡ ? ) |
mr2_plus ( ? + ? ) |
mr2_minus ( ? ▭ ? ≡ ? ) |
|
|
|
|
|
|
|
extensions to the library |
|
stream ( ? @ ? ) |
stream_eq ( ? ≐ ? ) |
stream_hdtl ( ↓? ) |
stream_tls ( ↓*[?]? ) |
|
|
|
|
|
|
|
|
|
list ( ◊ ) ( ? @ ? ) ( |?| ) |
list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) |
|
|
|
|
|
|
|
|
|
|
|
bool ( Ⓕ ) ( Ⓣ ) |
arith ( ?^? ) ( ⫯? ) ( ⫰? ) |
|
|
|
|
|
|
|
|
|
|
|
star |
lstar |
|
|
|
|
|
|
|
|
|
generated logical decomposables |
|
xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ ) |
xoa_props ( ⊥ ) ( ⊤ ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Last update: Fri, 04 Mar 2016 20:49:20 +0100