Interface | Description |
---|---|
Command |
Interface to commands.
|
ProofCommand |
Interface to proof commands.
|
Class | Description |
---|---|
Assume |
Commnand "assume": split proof state by an assumption and its proof.
|
Auto |
Command "auto": try to close state by automatic instantiation
of quantified formulas.
|
AutoStar |
command "autostar": apply auto to current node and its successor siblings.
|
Case |
The "case" command: split state into multiple cases.
|
CommandBase |
Base class of commands.
|
ContextC |
Command "newcontext": change context to denoted path.
|
CounterExample |
Command "counterexample": show potential counterexample for current
state (may be time-consuming)
|
DeclarationC |
Virtual command "declaration": process declaration in current environment
|
Decompose |
command "decompose": decompose proof state by repeated skolemization
and flattening.
|
Empty |
The virtual "empty" command: do nothing.
|
EnvironmentC |
Command "environment": show environment (global or of current state).
|
Expand |
Command "expand": expand a definition.
|
Flatten |
Command "flatten": decompose compound formulas without splitting the state.
|
Flip |
Command "flip": flip a formula from goal position to assumption position
or vice versa.
|
FormulaC |
Command "formula": print value of formula identifier.
|
Goal |
Command "goal": let a formula become the single goal.
|
Goto |
The "goto" command: goto an open proof state.
|
Induction |
Command "induction": induction on a univerally quantified NAT/INT variable.
|
Instantiate |
The "instantiate" command: instantiate a quantified formula.
|
Lemma |
The "lemma" command: import other formulas.
|
Next |
The "next" command: goto next open proof state.
|
Open |
The "open" command: display the list of open states.
|
Option |
The "option" command: set a system option.
|
Prev |
The "prev" command: goto previous open proof state.
|
ProofC |
Command "proof": print proof tree.
|
ProofCommandBase |
Base class of proof commands.
|
Prove |
"prove": prove goal formula.
|
Proved |
Pseudo-command "proved": indicate the termination of a proof branch.
|
Quit |
"quit": quit from current proof or session.
|
Read |
Command "read": read command from denoted file.
|
Redo |
The "redo" command: goto an open proof state and redo its proof.
|
Scatter |
command "scatter": scatter proof state by repeated decomposition
and goalsplitting.
|
Simplify |
Command "simplify": simplify a proof state.
|
Skolemize |
Command "skolemize": skolemize universal formulas in goal position and
existential formulas in assumption position.
|
Split |
Command "split": split a proof state.
|
StateC |
Command "state": print denoted state.
|
TCC |
"tcc": print type checking conditions generated from last declaration.
|
TypeAxiom |
The "typeaxiom" command: instantiate a quantified type axiom.
|
TypeC |
Command "type": print value of type identifier.
|
Undo |
The "undo" command: goto a closed proof state and undo its proof.
|
ValueC |
Command "print": print value of value identifier.
|