package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

sha256=bd1d61581eed552aef1b2a37442684a9f96240f1faaf695330c33391a8742a4a

sha512=44566902af1ef750d901527b4b9f5ef9872cfed88a935fe94a78e5a07692855949fed5d71e6709a19f5bf619cf3640391f393fdfeaa98834e72c35106af460c3

Sourcemodule Stats : sig ... end

val interp_command : 
  st:Coq.State.t ->
  Coq.Ast.t ->
  Coq.State.t Coq.Interp.interp_result Stats.t

Interpret a command, possibly memoizing it

Sourceval interp_admitted : st:Coq.State.t -> (Coq.State.t, Loc.t) Coq.Protect.E.t

Sourceval mem_stats : unit -> int

Stats

Sourcemodule CacheStats : sig ... end

Sourceval load_from_disk : file:string -> unit

Not working yet

Sourceval save_to_disk : file:string -> unit

Sourceval input_info : (Coq.Ast.t * Coq.State.t) -> string

debug