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.0.8.19.tbz

sha256=01ffedbd55ae00526fe1dda890e3c15a883bfda8388c8d292121ee722db46360

sha512=b5d92146c27b5c432a3f92c9ae8ff69c4dc62709f394743ca2d43ab93ae3af64b08bb17ea5923c0fbe0a333de127de574c548ec3c8df81dbe3e11f485abc3216

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