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;