Theory Index and Theory Page Format Descriptions

Theory Index Format Description

1. Number of definitions in theory.
2. Number of theorems in theory. This includes all the well-formedness theorems.
3. Number of lines of proof-scripts for generating proofs of all theorems in theory. This excludes comments and blank lines.

Theory Page Format Description

Introduction

Describes the contents of the theory.

Summary of Definitions

Gives the names of definitions introduced in the theory, and gives for each definition an example of how it is usually displayed. Some display forms for definitions optionally hides one or more arguments, then two example displays are given; one with the hiding enabled, the other with it disabled. This hiding can be interactively controlled by setting the value of a switch.

Typed Definitions

Each Nuprl definition usually comes in three parts; one or more display forms that govern how it is displayed, the definition itself called an abstraction , and a well-formedness lemma that gives the type of the definition.

The first item in a typed definition is a lemma that combines the information normally presented in the abstraction and the well-formedness lemma. Some definitions have multiple well-formedness lemmas, in which case the second and subsequent lemmas are also presented.

Type checking of definitions is accomplished by proof. After the definition name are one or more `*'s, each followed by a number. Each of these is a link to a display of the proof of a well-formedness lemma for the definition. The number indicates the number of lines in the proof-script for generating the proof of the lemma.

A few definitions don't have any well-formedness lemma. In this case, just the left- and right-hand sides of the definition's abstraction are presented on either side of a == .

Main Theorems

The main theorems of the theory are presented here. Follow the * links to view the proofs of these theorems. Occasionally the link will have a ? instead. This indicates that the proof is incomplete, and therefore that the goal presented might possibly be unprovable. After the * or ? symbol is a number indicating the number of lines in the proof-script for generating the proof of the theorem.

Listing

This link leads to a listing of every object in the theory, without the proofs being shown. These listings show other kinds of theory objects, such as ML objects and the display form objects that introduce the display forms for definitions.