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

Here is a numerical account of the specification's contents and its timeline.

category	objects
sizes	files	27	characters	48334	nodes	67588
propositions	theorems	2	lemmas	201	total	203
concepts	declared	40	defined	24	total	64

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 ( ? + ? )
extensions to the library		star	lstar	bool ( Ⓕ ) ( Ⓣ )	arith ( ?^? )	list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )
generated logical decomposables		xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )	xoa_props ( ⊥ ) ( ⊤ )