package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.2.8.18.tbz
sha256=ec0a692c2ca60ee1a087626bb6087076f0e9a5ace3c88b1209c2f5dea0c91035
sha512=8aac7c4c99a7bdae741084e567348f8a4c36d64939d79348ff7b6f50dacf36da7aee8b7e648e94a863e895d1c60d911e2b3e38b4b8dcdf04c8ed1edde28f7660
doc/coq-lsp.coq/Coq/Library_file/index.html
Module Coq.Library_file
Source
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.
Recovers the list of loaded libraries for state st
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>