%clause

From The Twelf Project
Jump to: navigation, search

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

This function of Twelf is incompatible with Twelf'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 Twelf, and the article on that subject has an example of %clause being used.

See also