%clause

The %clause keyword allows a constant that is defined to be used by STELF during proof search. If %clause is not used, then STELF will only perform proof search on constants that are declared in the signature.

This function of STELF is incompatible with STELF’s ability to prove metatheorems, and so type families that use %clause or depend on other type families that use %clause cannot be a part of directives that specify totality assertions such as %total. It has mostly been used to do tactical theorem proving in STELF, and the article on that subject has an example of %clause being used.

See also

• Clause Definitions (guide §5.29)
• Tactical theorem proving