fmrisc.ProofNavigator.Commands

Interface ProofCommand

All Superinterfaces:

Command

All Known Implementing Classes:

Assume, Auto, AutoStar, Case, CounterExample, Decompose, Expand, Flatten, Flip, Goal, Goto, Induction, Instantiate, Lemma, Next, Open, Option, Prev, ProofCommandBase, Proved, Redo, Scatter, Simplify, Skolemize, Split, TypeAxiom, Undo

public interface ProofCommand
extends Command

Interface to proof commands.

Method Summary

Modifier and Type	Method and Description
ProofState[]	process(ProofState state) process proof state.

Methods inherited from interface fmrisc.ProofNavigator.Commands.Command

process, toNode

Method Detail

process

ProofState[] process(ProofState state)

process proof state.

Parameters:

state - the state to which the proof command is applied (remains unchanged)

Returns:

a sequence of children of state generated by the command (null, if the command did not generate any)