Nuprl Browsing

In a hurry? See HOW to do various things.

This material is a projection of part of the library of mathematics developed by the Cornell Nuprl project.

The material is organized into "Sections" which may refer to prior sections. Each section comprises a collection of library objects, which may be definitions, proofs, or informal documents. The items on the Nuprl Math Library page refer to sections, conglomerations of sections, or to individual objects within sections. The "book" image connotes a larger body than the "pamphlet" image. Some "pamphlets" are simply especially interesting excerpts from "books."

There are several kinds of pages:

Main Page for a Section e.g. NuprlPrimitives, rel 1

List of Prior Sections e.g. those preceding int 2

Inference Step of a Proof e.g. an internal proof step; a proof top.

Print Form of a Proof e.g. printform for Thm* x:. y:. yyx & x < (y+1)(y+1).

Lemma Citations from a Proof e.g. for a proof about remainders..

Definitions e.g. for ; for y greater-bounds x; for section int 1.

Thms and Defs Using an Operator e.g. mentions of |x| in int 2.

Miscellaneous Informal Documents e.g. an explanation of pairing.

Generally, a page will include a list of one or more links in the upper and lower right hand corners. Here are some kinds of links you may find there:

"Doc" points to this browsing documentation.
"Remark" points to remarks pertinent to the page content,
e.g. a technical remark; a remark on methodology; a historical remark
"Definitions" points to a collection of definitions appropriate to the page.
A Section name points to its Main Page .
Some larger organizational context will be indicated.
Other kinds of links are specific to the kind of page.

At the bottom of most pages, as on this one, there appears a spattering of links depicting basic operators of the Nuprl language that appear on the page. These lead to a rather large body of explanation of Nuprl primitives and basic methods of mathematical expression in Nuprl. There is an Index to that basic documentation.

HOW to do various things.

About:

NuprlLib Acknowledgment

Main Page for a Section	e.g. NuprlPrimitives, rel 1
List of Prior Sections	e.g. those preceding int 2
Inference Step of a Proof	e.g. an internal proof step; a proof top.
Print Form of a Proof	e.g. printform for Thm* x:. y:. yyx & x < (y+1)(y+1).
Lemma Citations from a Proof	e.g. for a proof about remainders..
Definitions	e.g. for ; for y greater-bounds x; for section int 1.
Thms and Defs Using an Operator	e.g. mentions of \|x\| in int 2.
Miscellaneous Informal Documents	e.g. an explanation of pairing.