Showing a Unit

When a unit definition is elaborated, a unit value is produced. For example, a spec is essentially a set of types, ops, and axioms. A spec can be constructed by means of various operations in the Metaslang language, but the final result is always a spec, i.e., a set of types, ops, and axioms.

The command for showing unit values is:

show [unit-term]

As for proc the argument can be any unit term: a simple unit identifier, a diagram colimit, a proof term, and so on, and a missing argument means: use the last argument supplied in a unit-term position. However, unlike for proc, the argument can not be a multi-unit identifier.

The unit term is processed as for the proc command. If no error occurred, the unit value resulting from elaborating the unit term is shown on the output. However, an attempt is made to keep imported specs as import declarations, instead of expanded in the output. If the argument was already a spec form, the output may look different in several ways: white space may be different, declarations may have been added or re-ordered, and explicit qualifications may have been added.

To show imported specs expanded in place, use:

showx [unit-term]

(for SHOW eXpanded).

"Showing" a proof unit has the same effect as just processing it; the elaboration of a proof unit is only in the side effects.