%theorem

The %theorem declaration is an alternative way of specifying metatheorems in STELF. It is not fully supported or documented, but some prefer the syntax for its clarity when proving 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 STELF 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

• Theorem prover
• Theorem Prover (guide §10.57)