package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.4.0.tbz
sha256=739cab9a0a6c3ab0e7df210fb6fdcdb749a6fa70aa7ca59145da177c25428cb6
sha512=f1413e65259d1587d57d656a5153890c355fa339d981c0b038736bcaf53c698cc10466fbc77444d103c7b6ccb8d63290ff80a506d057bc199a29d53947e898c9

doc/lambdapi.pure/Pure/index.html

Module PureSource

Interface to LSP.

Sourcemodule Command : sig ... end

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

Sourcemodule Tactic : sig ... end

Abstract representation of a tactic (proof item).

Sourcemodule ProofTree : sig ... end

Abstract representation of a proof.

Sourcetype state

Representation of the state when at the toplevel.

Sourcetype proof_state

Representation of the state when in a proof.

Sourceexception Parse_error of Common.Pos.pos * string

Exception raised by parse_text.

Sourceval parse_text : state -> fname:string -> string -> Command.t list * state

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.

Sourcetype conclusion =
  1. | Typ of string * string
    (*

    Metavariable name and type.

    *)
  2. | Unif of string * string
    (*

    LHS and RHS of the unification goal.

    *)

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

Sourcetype goal = (string * string) list * conclusion
Sourceval current_goals : proof_state -> goal list

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

Sourcetype command_result =
  1. | Cmd_OK of state * string option
    (*

    Command is done.

    *)
  2. | Cmd_Proof of proof_state * ProofTree.t * Common.Pos.popt * Common.Pos.popt
    (*

    Enter proof mode (positions are for statement and qed).

    *)
  3. | Cmd_Error of Common.Pos.popt option * string
    (*

    Error report.

    *)

Result type of the handle_command function.

Sourcetype tactic_result =
  1. | Tac_OK of proof_state * string option
  2. | Tac_Error of Common.Pos.popt option * string

Result type of the handle_tactic function.

Sourceval initial_state : string -> state

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

Sourceval handle_command : state -> Command.t -> command_result

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).

Sourceval handle_tactic : proof_state -> Tactic.t -> int -> tactic_result

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.

Sourceval set_initial_time : unit -> unit

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.