object.rst

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 <objectidentifier>. The object command is terminated with a ; character.

Behavior

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

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

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;