%trustme

From The Twelf Project

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.

[edit] See also

• Holes in metatheorems

Twelf keywords

---

%. %abbrev %assert %block %clause %covers %define %deterministic %establish %freeze %infix %prefix %postfix %mode %name %prove %query %querytabled %reduces %solve %subord %tabled %terminates %thaw %theorem %total %trustme %unique %use %worlds