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-project

Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

Maintainers

E

e@x80.org

Sources

coq-lsp-0.2.5+8.20.tbz

sha256=764f5cbaf3da308a21ea2953a275e74b6e5a841c82bdd8b71fa474b1395738a1

sha512=16189385a27ce7576820d03d4410d4f9bc52150b43d714813c3611d6b5519b5d256c1ac348913bbf77c6f313d54927ead935a188783e04b21032f5e06c793778

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