# %theorem

From The Twelf Project

The ** %theorem** declaration acts as the

*specification*of a theorem.

This article or section needs syntax of the declaration. |

## Use to write statements of metatheorems

Some people find the notation a clearer way of specifying metatheorems; a `%theorem` declaration used in this style handles the type family declation and the `%mode` declaration parts of a totality assertion.

## Use with the theorem prover

When using the Twelf theorem prover, a `%theorem` declaration establishes a proposition that the theorem prover may later attempt to establish. A ** %theorem** declaration is thus somewhat analogous to the three-part specification of a totality assertions, the type family definition, the %mode declaration, and the %worlds declaration.