| Copyright | uni-bremen and DFKI |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | r.pascanu@jacobs-university.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CMDL.ProveCommands
Description
CMDL.ProveCommands contains all commands (except prove/consistency check) related to prove mode
Synopsis
- cTranslate :: String -> CmdlState -> IO CmdlState
- cDropTranslations :: CmdlState -> IO CmdlState
- cGoalsAxmGeneral :: CmdlListAction -> CmdlGoalAxiom -> String -> CmdlState -> IO CmdlState
- cDoLoop :: ProveCmdType -> CmdlState -> IO CmdlState
- cProve :: CmdlState -> IO CmdlState
- cDisprove :: CmdlState -> IO CmdlState
- cProveAll :: CmdlState -> IO CmdlState
- cSetUseThms :: Bool -> CmdlState -> IO CmdlState
- cSetSave2File :: Bool -> CmdlState -> IO CmdlState
- cEndScript :: CmdlState -> IO CmdlState
- cStartScript :: CmdlState -> IO CmdlState
- cTimeLimit :: String -> CmdlState -> IO CmdlState
- cNotACommand :: String -> CmdlState -> IO CmdlState
- cShowOutput :: Bool -> CmdlState -> IO CmdlState
Documentation
cTranslate :: String -> CmdlState -> IO CmdlState Source #
select comorphisms
cDropTranslations :: CmdlState -> IO CmdlState Source #
Drops any seleceted comorphism
cGoalsAxmGeneral :: CmdlListAction -> CmdlGoalAxiom -> String -> CmdlState -> IO CmdlState Source #
A general function that implements the actions of setting, adding or deleting goals or axioms from the selection list
cProve :: CmdlState -> IO CmdlState Source #
Proves only selected goals from all nodes using selected axioms
cProveAll :: CmdlState -> IO CmdlState Source #
Proves all goals in the nodes selected using all axioms and theorems
cSetUseThms :: Bool -> CmdlState -> IO CmdlState Source #
Sets the use theorems flag of the interface
cSetSave2File :: Bool -> CmdlState -> IO CmdlState Source #
Sets the save2File value to either true or false
cEndScript :: CmdlState -> IO CmdlState Source #
Function to signal the interface that the script has ended
cStartScript :: CmdlState -> IO CmdlState Source #
Function to signal the interface that a scrips starts so it should not try to parse the input
cTimeLimit :: String -> CmdlState -> IO CmdlState Source #
cNotACommand :: String -> CmdlState -> IO CmdlState Source #
The function is called everytime when the input could not be parsed as a command
cShowOutput :: Bool -> CmdlState -> IO CmdlState Source #