Library objects are collected into "sections" for presentation on the web. Each section comprises a collection of library objects, which may be definitions, proofs, or informal documents. Normally sections do not overlap. Often objects in one section refer to objects in another, prior, section; this relation is acyclic. Each section has a
Main Page
.
An example of a section is
bool 1.
Prior Sections
A section may depend upon "prior" sections, perhaps for definitions and lemmas. From the
Main Page
for a section that depends on prior sections one can find a list of those sections (e.g.
those preceding int 2
), along with brief descriptions of them, thru the "Sections" links in the right hand corners.
Normally when a series of sections is listed, it is (partially) ordered by dependency, the more dependent sections higher than their prior sections.
For example,
bool 1
depends on
int 1,
well fnd,
and
core.
Conglomerates
For further organizational structure, some "conglomerates" of other sections have been introduced, which are treated like sections in many ways. They are considered to comprise a collection of other sections and all their prior sections. Unlike true sections, conglomerates may overlap to the extent that distinct conglomerates may include common sections. Examples of conglomerates are StandardLIB, ClassicalPropLogic and Lists; the latter simply collects several disparate sections about lists under a convenient heading.
Larger Contexts
Each section is assigned a larger-context for convenience of navigation. Most pages of a section will include an "up-link" to this larger context in the right hand corners. This will typically be a link to a conglomerate or to the
Nuprl Math Library.