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

Dune Dependency

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

Authors

Maintainers

E

e@x80.org

Sources

coq-lsp-0.2.2.8.17.tbz

sha256=64c07c21284a6cf18c9c79fd614f188ebc552dd7a783a00e51c14cca8d062d07

sha512=9cc3efad65f5896af847880b74833c50897a7e4eba34f61e34b3c5136e237f53c6c38252aeb553b932d26e6b5b252631e758d8a8994c2b7c12cfa989fd5686ff

doc/coq-lsp.coq/Coq/Library_file/index.html

Module `Coq.Library_file`Source

Sourcetype t

Sourceval name : t -> Names.DirPath.t

Logical path of the library

Sourcemodule Entry : sig ... end

Source

val toc : 
  token:Limits.Token.t ->
  st:State.t ->
  t list ->
  (Entry.t list, Loc.t) Protect.E.t

toc libs Returns the list of constants and inductives found on .vo libraries libs, as pairs of name, typ. Note that the constants are returned in the order they appear on the file.

NOTE that (unfortunately) this is a very expensive process, similary to Coq's Search, as this routine will have to traverse all the library objects in scope.

Hence, we provide a slightly more efficient version that can do multiple libraries but with the same complexity.

There have been several upstream Coq PRs trying to improve this situation, but so far they didn't make enough progress.

Sourceval loaded : token:Limits.Token.t -> st:State.t -> (t list, Loc.t) Protect.E.t

Recovers the list of loaded libraries for state st