Abstract representation of a command (top-level item).

Abstract representation of a tactic (proof item).

Abstract representation of a proof.

Representation of the state when at the toplevel.

Representation of the state when in a proof.

parse_text ~fname contents runs the parser on the string contents as if it were a file named fname. It returns the list of commands it could parse and, either None if it could parse all commands, or some position and error message otherwise.

A goal is given by a list of assumptions and a conclusion. Each assumption has a name and a type.

current_goals s returns the list of open goals for proof state s.

Result type of the handle_command function.

Result type of the handle_tactic function.

initial_state fname gives an initial state for working with the (source) file fname. The resulting state can be used by handle_command.

handle_command st cmd evaluates the command cmd in state st, giving one of three possible results: the command is fully handled (corresponding to the Cmd_OK constructor, the command starts a proof (corresponding to the Cmd_Proof constructor), or the command fails (corresponding to the Cmd_Error constuctor).

handle_tactic ps tac n evaluates the tactic tac with n subproofs in proof state ps, returning a new proof state (with Tac_OK) or an error (with Tac_Error).

end_proof st finalises the proof which state is st, returning a result at the command level for the whole theorem. This function should be called when all the tactics have been handled with handle_tactic. Note that the value returned by this function cannot be Cmd_Proof.

get_symbols st returns all the symbols defined in the signature at state st. This can be used for displaying the type of symbols.

set_initial_time () records the current imperative state as the rollback "time" for the initial_state function. This is only useful to initialise or reinitialise the pure interface.