package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.1.v8.16.tbz
sha256=be48fd1449d8a0eb209e83ebbcde95090e94ba74ee7e744a399c3a5b67cc4acb
sha512=c711b953346d3e45ed61c75d5f3825d877820dec38e5dc803cd1ab9a32d6b4a850232a84984c3c340d3939c459ea0595f606d303e1ba714e4245a784b3507ab0
doc/coq-lsp.coq/Coq/Init/index.html
Module Coq.Init
Source
Source
type coq_opts = {
fb_handler : Feedback.feedback -> unit;
(*callback to handle async feedback
*)load_module : string -> unit;
(*callback to load cma/cmo files
*)load_plugin : Mltop.PluginSpec.t -> unit;
(*callback to load findlib packages
*)debug : bool;
(*Enable Coq Debug mode
*)
}
Source
val doc_init :
root_state:State.t ->
workspace:Workspace.t ->
libname:Names.DirPath.t ->
require_libs:
(string * string option * Vernacexpr.export_with_cats option) list ->
State.t
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>