Also see Canonical Forms for newer supplementary material.

next up previous contents index
Next: Stating Theorems Up: Syntactic Issues Previous: Theorems

Expressions Formed by Using Type Constructors

The basic components of the type theory employed by the Nuprl system are the atomic  types int, atom and void. In addition to the atomic types, there is an integer--indexed family of predefined types called universes , . Universes are types whose canonical elements are types. All the atomic types are members of , and is a member of . More complex types are built from the atomic types and the universes by using type  constructors, operators which take types and build new types from them. The type constructors used in Nuprl aregif

The meaning of these type constructors has been briefly discussed in chapter 2 and will be discussed in detail in chapter 8. The first three type constructors are binary, and all have equal precedence .  They all associate  to the right. We can also form types by using the forms `` element in type'' and `` element = element in type''. As explained in chapter 2, these are two of the basic judgement  forms. The symbols in and = can be viewed as a type constructor for the purposes of the present discussion. Viewed in this way, in associates to the left. The symbol = binds more tightly than the symbol in. The type constructors in the list above also bind more tightly than does in. The binding and scope conventions are described in chapter 2.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995