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.fleche/Fleche/Doc/Env/index.html

Module `Doc.Env`Source

Enviroment external to the document, this includes for now the init Coq state and the workspace, which are used to build the first state of the document, usually by importing the prelude and other libs implicitly.

Sourcetype t = private {

init : Coq.State.t;
workspace : Coq.Workspace.t;
files : Coq.Files.t;

}

Source

val make : 
  init:Coq.State.t ->
  workspace:Coq.Workspace.t ->
  files:Coq.Files.t ->
  t

Sourceval inject_requires : extra_requires:Coq.Workspace.Require.t list -> t -> t