From The Twelf Project
Jump to: navigation, search

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.

See also