package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val name : t -> Names.DirPath.t

Logical path of the library

module Entry : sig ... end
val toc : token:Limits.Token.t -> st:State.t -> t list -> (Entry.t list, Loc.t) Protect.E.t

toc libs Returns the list of constants and inductives found on .vo libraries libs, as pairs of name, typ. Note that the constants are returned in the order they appear on the file.

NOTE that (unfortunately) this is a very expensive process, similary to Coq's Search, as this routine will have to traverse all the library objects in scope.

Hence, we provide a slightly more efficient version that can do multiple libraries but with the same complexity.

There have been several upstream Coq PRs trying to improve this situation, but so far they didn't make enough progress.

val loaded : token:Limits.Token.t -> st:State.t -> (t list, Loc.t) Protect.E.t

Recovers the list of loaded libraries for state st

val locate_absolute_library : Names.DirPath.t -> (string, Exninfo.iexn) Result.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct