%use

From The Twelf Project

A %use directive adds a constraint domain to the current Twelf signature.

Like some other directives, for instance %clause, it is incompatible with Twelf's ability to verify totality assertions and metatheorems.

[edit] See also

• Constraint domains
• Constraint domains in the User's Guide

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