%trustme

From The Twelf Project
Jump to: navigation, search
This article or section describes an undocumented feature of Twelf.
The information may be incomplete and subject to change.
The %trustme keyword, when it precedes another directive such as a %total directive, causes Twelf to believe that the directive succeeded even if it did not. This feature is only available in unsafe mode, and can be used to easily create holes in metatheorems.

See also