[lambdadelta home]
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
[Spacer]

home news specification

documentation implementation
foreword milestones version 2 (background - core - applications)
version 2 library (static LDDL directory)
citations visibility version 1 (background - core) (static HELM directory) version 1 helena
Summary of the Specification [spacer]
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
Logical Structure of the Specification [spacer]
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 ( ⊥ ) ( ⊤ )









[Spacer]

[Valid XHTML 1.1] [Valid CSS level 2] [Generated from XML via XSL] [PNG used here] [Viewable with any browser]

Last update: Wed, 14 Oct 2015 21:43:44 +0200