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
  - Goals
  - Init
  - Interp
    
    Info
  - Loader
  - Message
  - Parsing
    
    Parsable
  - Print
  - Protect
    
    E
    
    Error
    
    R
  - State
    
    Proof
  - Workspace
    
    CmdLine
coq-lsp.fleche
- Fleche
  - Config
  - Debug
  - Doc
    
    Completion
    
    Node
    
    Info
    
    Target
  - Info
    
    LC
    
    LineCol
    
    O
    
    Offset
    
    Point
    
    S
    
    P
  - Io
    
    CallBack
    
    Log
    
    Report
  - Memo
    
    CacheStats
    
    Stats
  - Stats
    
    Kind
  - Types
    
    Diagnostic
    
    Extra
    
    Point
    
    Range
coq-lsp.lsp
- Lsp
  - Base
    
    Message
  - Io
    
    TraceValue

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 payload = Loc.t option * Pp.t

type t = private

| User of payload
| Anomaly of payload