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
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
    
    Admit
    
    CacheStats
    
    Init
    
    Interp
    
    Stats
  - Progress
    
    Info
  - Stats
    
    Kind
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

Legend:
Library
Module
Module type
Parameter
Class
Class type

type 'a hyp = 'a Coq.Goals.hyp = {

names : string list;
def : 'a option;
ty : 'a;

}

val hyp_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a hyp -> Yojson.Safe.t

val hyp_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a hyp Ppx_deriving_yojson_runtime.error_or

type info = Coq.Goals.info = {

evar : Evar.t;
name : Names.Id.t option;

}

val info_to_yojson : info -> Yojson.Safe.t

val info_of_yojson : Yojson.Safe.t -> info Ppx_deriving_yojson_runtime.error_or

type 'a reified_goal = 'a Coq.Goals.reified_goal = {

info : info;
hyps : 'a hyp list;
ty : 'a;

}

val reified_goal_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a reified_goal ->
  Yojson.Safe.t

val reified_goal_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a reified_goal Ppx_deriving_yojson_runtime.error_or

module Goals_ : sig ... end

type ('a, 'pp) goals = ('a, 'pp) Coq.Goals.goals

val goals_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  ('b -> Yojson.Safe.t) ->
  ('a, 'b) Coq.Goals.goals ->
  Yojson.Safe.t

type 'pp reified_pp = ('pp reified_goal, 'pp) goals

val reified_pp_to_yojson : 
  'pp. ('pp -> Yojson.Safe.t) ->
  'pp reified_pp ->
  Yojson.Safe.t

val _ : ('a -> Yojson.Safe.t) -> 'a reified_pp -> Yojson.Safe.t