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.5.8.16.tbz

sha256=5a0819d6ceb18cf031ece2c466eefd27f018d85c1c7472038bbb7c2663714b6e

sha512=be97b25db922014681dce75a68566b887f692c60208b698f03ce8b2fc0c1a2eab5c0c563d698eeb1d21dea5405468e958e67cce9a6c94a3106529f1b4ebfce13

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 goals = 'a Coq.Goals.goals

Source

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

Sourcetype reified_pp = Pp.t reified_goal goals

Sourceval reified_pp_to_yojson : reified_pp -> Yojson.Safe.t

Sourceval _ : 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