package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

coq-lsp.coq
- Coq
  - Ast
    
    Id
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
    
    Info
  - Goals
  - Init
  - Interp
    
    Info
  - Loader
  - Message
  - Parsing
    
    Parsable
  - Print
  - Protect
    
    E
    
    Error
    
    R
  - State
    
    Proof
  - Utf8
  - Utils
  - Workspace
    
    CmdLine
coq-lsp.fleche
- Fleche
  - Config
    
    Unicode_completion
  - Contents
    
    R
  - Debug
  - Doc
    
    Completion
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Target
  - Info
    
    LC
    
    LineCol
    
    O
    
    Offset
    
    Point
    
    S
    
    P
  - Io
    
    CallBack
    
    Log
    
    Report
  - Memo
    
    CacheStats
    
    Stats
  - Progress
    
    Info
  - Stats
    
    Kind
coq-lsp.fleche.waterproof
- Fleche_waterproof
  - Json
    
    CAst
  - Ljson
  - Tjson
coq-lsp.lang
- Lang
  - Diagnostic
    
    Extra
  - LUri
    
    File
  - Point
  - Range
coq-lsp.lsp
- Lsp
  - Base
    
    Message
  - Doc
    
    VersionedTextDocument
  - Io
    
    TraceValue
  - JCoq
    
    Goals
    
    Goals_
    
    Pp
  - JFleche
    
    CompletionData
    
    Config
    
    DocumentSymbol
    
    GoalsAnswer
    
    HoverContents
    
    HoverInfo
    
    LabelDetails
    
    Location
    
    LocationLink
    
    Message
    
    SymInfo
    
    TextEditReplace
  - JLang
    
    LUri
    
    File
    
    Point
    
    Range

Legend:
Library
Module
Module type
Parameter
Class
Class type

type t = {

line : int;
character : int;
offset : int;

}

ATTENTION: character is a Unicode caracter position, thus from Coq that usually requires conversion, as it will report the column offset in bytes. But offset is in bytes for now, as our downstream clients prefer this format.

val pp : Format.formatter -> t -> unit