package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

package coq-lsp

coq-lsp.coq
- Coq
  - Ast
    
    Id
    
    Map
    
    Monad
    
    M
    
    Smart
  - Goals
  - Init
  - Interp
  - Loader
  - Message
  - Parsing
    
    Parsable
  - Print
  - Protect
    
    E
    
    Error
    
    R
  - Save
  - State
    
    Proof
  - Utf8
  - Utils
  - Workspace
    
    CmdLine
    
    Flags
    
    Warning
coq-lsp.fleche
- Fleche
  - Config
    
    Unicode_completion
  - Contents
    
    R
  - Debug
  - Doc
    
    Completion
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Target
  - Info
    
    Completion
    
    Goals
    
    LC
    
    LineCol
    
    O
    
    Offset
    
    Point
    
    S
    
    P
  - Io
    
    CallBack
    
    Log
    
    Report
  - Memo
    
    Admit
    
    CacheStats
    
    Init
    
    Interp
    
    Stats
  - Perf
    
    Sentence
  - Perf_analysis
  - Progress
    
    Info
  - Stats
    
    Kind
  - Theory
    
    Check
    
    Register
    
    Completed
    
    Request
  - Version
coq-lsp.fleche.waterproof
- Fleche_waterproof
  - Json
    
    CAst
  - Ljson
  - Tjson
coq-lsp.lang
- Lang
  - Ast
    
    Info
    
    Name
  - Diagnostic
    
    Extra
  - LUri
    
    File
  - Point
  - Range
  - With_range
coq-lsp.lsp
- Lsp
coq-lsp.plugin.example
- Example_plugin
  - Main

Legend:
Library
Module
Module type
Parameter
Class
Class type

This modules reifies Coq side effects into an algebraic structure.

This is obviously very convenient for upper layer programming.

As of today this includes feedback and exceptions.

type 'l payload = 'l option * Pp.t

type 'l t = private

| User of 'l payload
| Anomaly of 'l payload