In order for Twelf to be useful as a theorem verifier, Twelf should not accept untrue or unproven assumptions. However, it is sometimes helpful for the Twelf user to be able to state, and use, unproven assumptions, especially during proof development. Directives like %trustme and %assert allow the Twelf user to do just this.
When Twelf is set to not accept any untrue or unproven assumptions, it is in safe mode (this is the default setting). In order to use directives like %trustme, Twelf must be set to unsafe mode.
Setting Twelf in unsafe mode
- In Twelf with Emacs, select the Twelf menu, then select the Options submenu, then select the unsafe menu option.
- If using the Twelf server directly from the command line, the command
set unsafe truewill put Twelf in unsafe mode.
- In ML Twelf, the SML command
Twelf.unsafe := true;will put Twelf in unsafe mode.