package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install

Dune Dependency

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

Authors

  1. E
    Emilio Jesús Gallego Arias <e@x80.org>
  2. A
    Ali Caglayan <alizter@gmail.com>
  3. S
    Shachar Itzhaky <shachari@cs.technion.ac.il>
  4. R
    Ramkumar Ramachandra <r@artagnon.com>

Maintainers

  1. E
    e@x80.org

Sources

coq-lsp-0.2.3.8.19.tbz
sha256=dd5d0993261d3742e77ccac8344307d97b507b265d8743ae0ce33d0b3fcfd98a
sha512=76727400b27900fdd659af7f03c5f2cd979f50ea0c76ad6f5b5de56a53b9db06dba1e1c786fd3e8ab695e42d94c53d58415c0c5b5eef8192f9863eaf7dcca693

doc/coq-lsp.serlib/Serlib/Ser_entries/index.html

Module Serlib.Ser_entriesSource

Sourcemodule Stateid = Ser_stateid
Sourcemodule Future = Ser_future
Sourcemodule Names = Ser_names
Sourcemodule Univ = Ser_univ
Sourcemodule UVars = Ser_uvars
Sourcemodule Constr = Ser_constr
Sourcemodule Declarations = Ser_declarations
Sourcemodule CPrimitives = Ser_cPrimitives
Sourcetype universes_entry = Entries.universes_entry =
  1. | Monomorphic_entry
  2. | Polymorphic_entry of UVars.UContext.t
Sourceval universes_entry_of_sexp : Sexplib0.Sexp.t -> universes_entry
Sourceval sexp_of_universes_entry : universes_entry -> Sexplib0.Sexp.t
Sourcetype 'a in_universes_entry = 'a * universes_entry
Sourceval in_universes_entry_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a in_universes_entry
Sourceval sexp_of_in_universes_entry : 'a. ('a -> Sexplib0.Sexp.t) -> 'a in_universes_entry -> Sexplib0.Sexp.t
Sourcetype one_inductive_entry = Entries.one_inductive_entry = {
  1. mind_entry_typename : Names.Id.t;
  2. mind_entry_arity : Constr.constr;
  3. mind_entry_consnames : Names.Id.t list;
  4. mind_entry_lc : Constr.constr list;
}
Sourceval one_inductive_entry_of_sexp : Sexplib0.Sexp.t -> one_inductive_entry
Sourceval sexp_of_one_inductive_entry : one_inductive_entry -> Sexplib0.Sexp.t
Sourcetype variance_entry = UVars.Variance.t option array
Sourceval variance_entry_of_sexp : Sexplib0.Sexp.t -> variance_entry
Sourceval sexp_of_variance_entry : variance_entry -> Sexplib0.Sexp.t
Sourceval proof_output_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a proof_output
Sourceval sexp_of_proof_output : 'a. ('a -> Sexplib0.Sexp.t) -> 'a proof_output -> Sexplib0.Sexp.t
Sourcetype definition_entry = Entries.definition_entry = {
  1. const_entry_body : Constr.constr;
  2. const_entry_secctx : Names.Id.Set.t option;
  3. const_entry_type : Constr.types option;
  4. const_entry_universes : universes_entry;
  5. const_entry_inline_code : bool;
}
Sourceval definition_entry_of_sexp : Sexplib0.Sexp.t -> definition_entry
Sourceval sexp_of_definition_entry : definition_entry -> Sexplib0.Sexp.t
Sourcetype section_def_entry = Entries.section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_type : Constr.types option;
}
Sourceval section_def_entry_of_sexp : Sexplib0.Sexp.t -> section_def_entry
Sourceval sexp_of_section_def_entry : section_def_entry -> Sexplib0.Sexp.t
Sourcetype inline = int option
Sourceval inline_of_sexp : Sexplib0.Sexp.t -> inline
Sourceval sexp_of_inline : inline -> Sexplib0.Sexp.t
Sourcetype 'a opaque_entry = 'a Entries.opaque_entry = {
  1. opaque_entry_body : 'a;
  2. opaque_entry_secctx : Names.Id.Set.t;
  3. opaque_entry_type : Constr.types;
  4. opaque_entry_universes : universes_entry;
}
Sourceval opaque_entry_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a opaque_entry
Sourceval sexp_of_opaque_entry : 'a. ('a -> Sexplib0.Sexp.t) -> 'a opaque_entry -> Sexplib0.Sexp.t
Sourcetype parameter_entry = Entries.parameter_entry = {
  1. parameter_entry_secctx : Names.Id.Set.t option;
  2. parameter_entry_type : Constr.types;
  3. parameter_entry_universes : universes_entry;
  4. parameter_entry_inline_code : inline;
}
Sourceval parameter_entry_of_sexp : Sexplib0.Sexp.t -> parameter_entry
Sourceval sexp_of_parameter_entry : parameter_entry -> Sexplib0.Sexp.t
Sourcetype primitive_entry = Entries.primitive_entry = {
  1. prim_entry_type : Constr.types in_universes_entry option;
  2. prim_entry_content : CPrimitives.op_or_type;
}
Sourceval primitive_entry_of_sexp : Sexplib0.Sexp.t -> primitive_entry
Sourceval sexp_of_primitive_entry : primitive_entry -> Sexplib0.Sexp.t
Sourcetype constant_entry = Entries.constant_entry =
  1. | DefinitionEntry : definition_entry -> constant_entry
  2. | ParameterEntry : parameter_entry -> constant_entry
  3. | PrimitiveEntry : primitive_entry -> constant_entry
Sourceval constant_entry_of_sexp : Sexplib0.Sexp.t -> constant_entry
Sourceval sexp_of_constant_entry : constant_entry -> Sexplib0.Sexp.t
Sourcetype module_struct_entry = (Constr.constr * UVars.AbstractContext.t option) Declarations.module_alg_expr
Sourceval module_struct_entry_of_sexp : Sexplib0.Sexp.t -> module_struct_entry
Sourceval sexp_of_module_struct_entry : module_struct_entry -> Sexplib0.Sexp.t
Sourcetype module_params_entry = (Names.MBId.t * module_struct_entry * inline) list
Sourceval module_params_entry_of_sexp : Sexplib0.Sexp.t -> module_params_entry
Sourceval sexp_of_module_params_entry : module_params_entry -> Sexplib0.Sexp.t
Sourcetype module_entry = Entries.module_entry =
  1. | MType of module_params_entry * module_struct_entry
  2. | MExpr of module_params_entry * module_struct_entry * module_struct_entry option
Sourceval module_entry_of_sexp : Sexplib0.Sexp.t -> module_entry
Sourceval sexp_of_module_entry : module_entry -> Sexplib0.Sexp.t
Sourcetype module_type_entry = module_params_entry * module_struct_entry
Sourceval module_type_entry_of_sexp : Sexplib0.Sexp.t -> module_type_entry
Sourceval sexp_of_module_type_entry : module_type_entry -> Sexplib0.Sexp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct