Twelf without Emacs
From The Twelf Project
First, you should read up on Twelf with Emacs, to understand how Twelf programs are divided up into files and how one interacts with those files. Then, instead of using emacs, you can run the twelf-server command directly from your shell and interact with your files using the following commands. (You may find it convenient to run twelf-server under some readline wrapper program like rlwrap or ledit to get command-line editing and history.)
Contents |
[edit] Loading the configuration file
To read your current config from sources.cfg, typemakeTo read some other config other.cfg, type
make other.cfg
[edit] Checking an individual declaration
To check an individual declaration, typereadDeclThen, on a new line, type a Twelf declaration, terminated with a period.
[edit] Checking an individual file
To load an individual file sometwelf.elf, typeloadFile sometwelf.elf
[edit] Logic programming proof search
To animate your specifications by doing logic programming queries, typetopYou will be presented with a a prompt,
?-at which you can type queries with existential metavariables, like
?- plus (s z) (s (s z)) N.Assuming you've loaded the signature from the Natural numbers article), the Twelf server responds with the following:
Solving...N = s (s (s z)).
More?
You can exit the logic programming top-level by pressing Ctrl-C.
[edit] Quitting
To quit from the Twelf server, typequitor press Ctrl-D.
