There are two kinds of definition listings. The first is simply a list of defined operators used in a library section . Each entry in this kind of list consists of

the left-hand side (definiendum) of the definition,

the name of the definition object, often connoting the meaning,

a pointer to the section in which it originates (unless it is the current section), and

a pointer to the definition itself (see "cascades" below).

These pages may be found with the "Definitions" button appearing the right hand corners of the Main Page for a Section , or a Definition Cascade, or a definition listing of this very sort when the current section is part of a larger "conglomerate section" to which it points as a larger context.

Definition Cascades

In order to speed up the tracing of definition chains, definitions are usually presented as a "cascade" of individual operator definitions . If the definition of an operator contains other defined operators on its right hand side (definiens) then the definitions of those operators are also shown below it. Example.

These definition cascade pages my be found with the "Definitions" buttons appearing in various other pages' corners, or by following citations of individual operator definitions occurring in text generally. The cascade for a single operator definition will contain only those definitions needed for that operator, whereas the "Definitions" button for a page may contain the cascade for most of the operators used in the page.

In addition to the definitions themselves, "well-formedness" theorems for the defined operators will be shown as well, which indicate the types of arguments and result of an operator. There may also be some remarks inserted.

In addition to the usual corner links, definition cascade pages may contain a "WhoCites" link, which points to a list of theorems and definitions mentioning the operator defined at the top of the cascade. This is handy for seeing what lemmas one has available.

As for undefined operators, i.e. primitives, links to explanations of cited primitives are provided at the bottoms of most pages.

Pseudo-primitives

Some defined operators are treated in this web representation, in some regards, as if they were primitives. Their definitions will often be omitted from cascades and from lists of defined operators mentioned in theorems and other definitions. This is usually because their definitions are reductions to type-theoretic concepts that are apt to be more distracting than useful to a casual browser. There are documents explaining these various operations accessible from documents or proofs that use them. See Pseudo-primitives for a listing of some of these operators.