package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

package coq-lsp

coq-lsp.coq
- Coq
  - Args
  - Ast
    
    Id
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
    
    Meta
    
    Command
    
    Require
  - Compat
    
    Ocaml_414
    
    In_channel
    
    Out_channel
    
    Result
    
    O
  - Files
  - Glob
    
    Info
  - Goals
  - Init
  - Interp
    
    Require
  - Library_file
    
    Entry
  - Limits
    
    Coq
    
    Token
    
    Intf
    
    Token
    
    Mp
    
    Token
    
    Token
  - Limits_mp_impl
    
    Token
  - Loader
  - Message
  - Parsing
    
    Parsable
  - Print
  - Protect
    
    E
    
    O
    
    Error
    
    R
  - Save
  - State
    
    Proof
  - Utils
  - Workspace
    
    CmdLine
    
    Flags
    
    Require
    
    Warning
coq-lsp.fleche
- Fleche
  - Config
    
    Unicode_completion
  - Contents
    
    R
  - Debug
  - Doc
    
    Completion
    
    Env
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Target
  - Info
    
    Completion
    
    Goals
    
    LC
    
    LineCol
    
    O
    
    Offset
    
    Point
    
    S
    
    P
  - Io
    
    CallBack
    
    Level
    
    Log
    
    Report
  - Memo
    
    Admit
    
    GlobalCacheStats
    
    Init
    
    Interp
    
    Require
    
    S
    
    Stats
  - Perf
    
    Info
    
    Sentence
  - Perf_analysis
  - Progress
    
    Info
  - ServerInfo
    
    Status
    
    Version
  - Stats
    
    Global
    
    Kind
  - Theory
    
    Check
    
    Register
    
    Completed
    
    InjectRequire
    
    Request
  - Version
coq-lsp.fleche.waterproof
- Fleche_waterproof
  - Json
    
    CAst
  - Ljson
  - Tjson
coq-lsp.lang
- Lang
  - Ast
    
    Info
    
    Name
  - Diagnostic
    
    Data
    
    Severity
  - LUri
    
    File
  - Point
  - Range
  - Utf
    
    Encoding
  - With_range
coq-lsp.lsp
- Lsp
coq-lsp.petanque
- Petanque
  - Agent
    
    Env
    
    Error
    
    Premise
    
    R
    
    Run_result
    
    State
coq-lsp.petanque.json
- Petanque_json
  - Client
    
    Chans
    
    S
    
    C
  - Interp
  - JAgent
    
    Env
    
    Error
    
    Goals
    
    Lang
    
    Range
    
    Premise
    
    R
    
    Run_result
    
    State
    
    Stdlib
    
    Result
  - Obj_map
    
    Make
    
    O
    
    Obj
    
    S
  - Protocol
    
    Goals
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Init
    
    Handler
    
    Response
    
    Params
    
    Response
    
    Message
    
    Params
    
    Notification
    
    S
    
    Params
    
    Premises
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Request
    
    S
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    RunTac
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Start
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Trace
    
    Params
  - Utils
coq-lsp.plugin.astdump
- Astdump_plugin
  - Main
coq-lsp.plugin.example
- Example_plugin
  - Main
coq-lsp.plugin.goaldump
- Goaldumpl_plugin
  - Main
coq-lsp.plugin.save_vo
- Savevo_plugin
  - Main

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