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

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

Source

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

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

Source

val reified_pp_of_yojson : 
  'pp. (Yojson.Safe.t -> 'pp Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'pp reified_pp Ppx_deriving_yojson_runtime.error_or

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `JCoq.Goals`Source

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