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

sha256=0b0ea3ce68aa549f61c004dd05d2b386dc18811ec4c9ac667ff2917857758707

sha512=d3e3ae7e055c1be38368fdc86679462e2aa4636805142e8fd1f73423a14a7c87e06d752f04964377fe39ed10972e3c47d433127694b104c0285adb976faadf66

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