package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (32)

Authors

Maintainers

E

e@x80.org

Sources

coq-lsp-0.1.7.8.18.tbz

sha256=c68fcee8101b40a1706c74ce2ca0386311aebb79ec1a96032fb51bc8b981314f

sha512=720ca5ba4f265d942232e8c2a85bd475f03bf7a592e1b9d6dfbd8c68689275ef2224b82310578bf430ad6b192ba5430ab11a62ef2524e3859c157a9680ac391b

doc/coq-lsp.lsp/Lsp/JCoq/Goals/index.html

Module `JCoq.Goals`Source

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

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

}

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

Source

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

Sourcetype info = Coq.Goals.info = {

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

}

Sourceval info_to_yojson : info -> Yojson.Safe.t

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

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

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

}

Source

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

Source

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

Sourcemodule Goals_ : sig ... end

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

Source

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

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

Source

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

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

package coq-lsp

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-lsp.lsp/Lsp/JCoq/Goals/index.html

Module JCoq.GoalsSource

Module `JCoq.Goals`Source