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.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8

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.

Sourceval parse_text : fname:string -> string -> Command.t list * (Common.Pos.pos * string) option

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.

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.