These are samples of expressions that we consider, whenever they are used, to be denoting discrete atomic entities, despite the fact that we can see characters constituting the expressions. The use of such characters permits some mnemonic exploitation.
However, there are no constructors or destructors in the theory for these atoms, nor is there a "new atom" generator. There is only a method for checking identity. If one uniformly replaced all the atom constants throughout a statement in Nuprl, preserving identity and difference, the result would still be true (or false) if the original was.
There is also an often-used
It's a bit subtle, in theory, but natural in practice.
There is no assumption pertaining to finiteness. One cannot prove that the type is finite or that it is not. However, for any number one can prove there are at least that many members of
Perhaps the best interpretation of
Another possible interpretation is as a primitive open-ended type whose members are introduced one-by-one as needed. Thus, one can always find a new member, but there's no systematic function for producing it. This seems as sensible as the intuitionistic notion of free choice sequence.