|
Ivor.Shell | Portability | non-portable | Stability | experimental | Maintainer | eb@dcs.st-and.ac.uk |
|
|
|
Description |
Shell interface to theorem prover
|
|
Synopsis |
|
|
|
Documentation |
|
|
|
|
|
|
|
Import a file of shell commands; fails if the module does not exist
in the current directory or search path, does nothing if already loaded.
|
|
|
Add a directory to the module search path
|
|
|
Add the standard library path to the module search path
|
|
|
Get the install prefix of the library
|
|
|
Get the system state from a finished shell
|
|
|
|
|
|
|
|
|
Send a command directly to a shell
|
|
|
Send a command directly to a shell, allowing commands which might
do IO actions.
|
|
|
:: String | Tactic name.
| -> String -> Tactic | Tactic function. The argument is whatever was input on the shell; the function is responsible for parsing this.
| -> ShellState | Shell to which to add the tactic.
| -> ShellState | | Add a user defined tactic to the shell.
|
|
|
|
:: String | Command name.
| -> String -> Context -> IO (String, Context) | Command function. The argument is whatever was input on the shell; the function is responsible for parsing this. The command returns a string (the response) and a possibly updated context.
| -> ShellState | Shell to which to add the command.
| -> ShellState | | Add a user defined command to the shell.
|
|
|
|
Add another parsing rule for parsing terms.
|
|
|
Set up the equality type, for use by the replace tactic
|
|
|
Parse a term using the shell's current parser extensions
|
|
|
Get a string representation of the current proof state
|
|
|
Get reply from last shell command
|
|
Produced by Haddock version 2.4.2 |