package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
doc/lambdapi.pure/Pure/index.html
Module Pure
Source
Interface to LSP.
Representation of the state when at the toplevel.
Representation of the state when in a proof.
Exception raised by parse_text
.
parse_text st ~fname contents
runs the parser on the string contents
as if it were a file named fname
. The action takes place in the state st
, and an updated state is returned. The function may raise Parse_error
.
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
.
type command_result =
| Cmd_OK of state * string option
(*Command is done.
*)| Cmd_Proof of proof_state * ProofTree.t * Common.Pos.popt * Common.Pos.popt
(*Enter proof mode (positions are for statement and qed).
*)| Cmd_Error of Common.Pos.popt option * string
(*Error report.
*)
Result type of the handle_command
function.
type tactic_result =
| Tac_OK of proof_state * string option
| Tac_Error of Common.Pos.popt option * string
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.