This is the so-called "standard" library of Nuprl objects. Most developments depend on much, though not all, of this material. After the NuprlLPE (logical programming environment) is fully deployed, it will be much easier to manage extensions to the "standard" material, but also it will be less important to have a single standard library.
| array 1 | |
| rat 1 | |
| num thy 1 | Elementary divisibility theory over the integers. Gcd function and relation introduced. Chinese remainder theorem proven. |
| list 1 | |
| int 2 | |
| rfunction 1 | |
| prog 1 | |
| sqequal 1 | |
| quot 1 | Support lemmas for quotient type. |
| rel 1 | Common properties of binary relations. |
| union | Non canonical functions (isl, outl, outr) for union type. |
| bool 1 | |
| int 1 | |
| well fnd | |
| fun 1 | |
| core | Some basic concepts defined type-theoretically. |
See also