package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.3.8.20.tbz
sha256=49a87d5fe263b3f8f7d2489f280db85e65890236c000e49ec9f41ab8edd266d5
sha512=1b7df9e7b29aa0a02864d7f06ad40deab1768e4ca2dc6ddb1719220276357eda14c272c5f4b47e4dc173d6a21272d6321c6a98a8647f251ed15bae9032da60d9
doc/coq-lsp.coq/Coq/Init/index.html
Module Coq.Init
Source
Source
type coq_opts = {
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
*)vm : bool;
(*Enable Coq's VM
*)warnings : string option;
(*Coq's Warnings
*)
}
Source
val doc_init :
token:Limits.Token.t ->
intern:Library.Intern.t ->
root_state:State.t ->
workspace:Workspace.t ->
uri:Lang.LUri.File.t ->
(State.t, Loc.t) Protect.E.t
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>