lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
module LSP = Lsp_base
val lp_logger : Buffer.t
type t = {
uri : string; |
version : int; |
text : string; |
mutable root : Pure.state; |
mutable final : Pure.state; |
nodes : doc_node list; |
logs : ((int * string) * Common.Pos.popt) list; |
map : Core.Term.qident Lplib.RangeMap.t; |
}
val mk_error : doc:t -> Common.Pos.pos -> string -> LSP.J.t
val buf_get_and_clear : Buffer.t -> string
val process_pstep :
(Pure.proof_state
* (Common.Pos.popt * int * string * Pure.goal list option) list
* ((int * string) * Common.Pos.popt) list) ->
Pure.Tactic.t ->
int ->
Pure.proof_state
* (Common.Pos.popt * int * string * Pure.goal list option) list
* ((int * string) * Common.Pos.popt) list
val process_proof :
Pure.proof_state ->
Pure.ProofTree.t ->
((int * string) * Common.Pos.popt) list ->
Pure.proof_state
* (Common.Pos.popt * int * string * Pure.goal list option) list
* ((int * string) * Common.Pos.popt) list
val process_cmd :
'a ->
(doc_node list
* Pure.state
* (Common.Pos.popt * int * string * Pure.goal list option) list
* ((int * string) * Common.Pos.popt) list) ->
Pure.Command.t ->
doc_node list
* Pure.state
* (Common.Pos.popt * int * string * Pure.goal list option) list
* ((int * string) * Common.Pos.popt) list
val new_doc : uri:string -> version:int -> text:string -> t
val dummy_loc : Common.Pos.pos Lazy.t