Theorem attributes

Theorem attributes are "tags" written in square brackets [] after a theorem name or reference. They can directly modify the theorem statement itself, or tag it to make it known to tools and automation.

Type checking and inference

The following attributes declare rules to be used by the type-checking and inference automation.

• [form]
• [intr]
• [elim]
• [comp]
• [type]

The typechecker's behavior is strongly linked to the particular way the rules it uses are formulated. In particular, the order of the premises of a rule dictates whether a particular step is a check or an inference, and so care should be taken to properly analyze the flow of type information when declaring a rule with one of the attributes above.

Logical reasoning

• [intro <n>]
• [elim <args>]

See also Methods § Logical reasoning