object

The object command is used to assert that an object exists.

Syntax

object [object identifier];
object [object identifier], [object identifier], ...;

The object identifier begins with the keyword object followed by one or more comma-separated object identifiers. The object command is terminated with a ; character.

Behavior

For each object identifier, an object is created in the current scope with the corresponding object identifier. For each such object, an object dependency is created in the current scope.

Because the object command creates dependencies, the object command may only be used in a global scope or a dependent scope.

Examples

In the default proofs library, the program naturals.core creates two objects NATURALS and ZERO using the commands:

object NATURALS;
object ZERO;

Which can be condensed into the single command:

object NATURALS, ZERO;