package coq-lsp

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

Install 

dune-project
 Dependency

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

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.5+9.0.tbz
sha256=11ba9a2f5c25f55fdfe1c00072f89940e35bd1441c64e2adac388a1cda53c881
sha512=b13d76d054c47354032d3371db8ff8bc2fbc78e2509596733249ebca8a2f5ce94529fcdb76cce0a353ecea26f66a52cd2b51310dad9156be10de7fe2ee66f6ba

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

Module Serlib.Ser_constrSource

Sourcetype metavariable = Constr.metavariable
Sourceval metavariable_of_sexp : Sexplib.Sexp.t -> metavariable
Sourceval sexp_of_metavariable : metavariable -> Sexplib.Sexp.t
Sourcetype pconstant = Constr.pconstant
Sourceval pconstant_of_sexp : Sexplib.Sexp.t -> pconstant
Sourceval sexp_of_pconstant : pconstant -> Sexplib.Sexp.t
Sourcetype pinductive = Constr.pinductive
Sourceval pinductive_of_sexp : Sexplib.Sexp.t -> pinductive
Sourceval sexp_of_pinductive : pinductive -> Sexplib.Sexp.t
Sourcetype pconstructor = Constr.pconstructor
Sourceval pconstructor_of_sexp : Sexplib.Sexp.t -> pconstructor
Sourceval sexp_of_pconstructor : pconstructor -> Sexplib.Sexp.t
Sourcetype cast_kind = Constr.cast_kind
Sourceval sexp_of_cast_kind : cast_kind -> Sexplib0.Sexp.t
Sourceval cast_kind_of_sexp : Sexplib0.Sexp.t -> cast_kind
Sourceval cast_kind_to_yojson : cast_kind -> Yojson.Safe.t
Sourceval hash_fold_cast_kind : Ppx_hash_lib.Std.Hash.state -> cast_kind -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_cast_kind : cast_kind -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_cast_kind : cast_kind -> cast_kind -> int
Sourcetype case_style = Constr.case_style
Sourceval sexp_of_case_style : case_style -> Sexplib0.Sexp.t
Sourceval case_style_of_sexp : Sexplib0.Sexp.t -> case_style
Sourceval case_style_to_yojson : case_style -> Yojson.Safe.t
Sourceval hash_fold_case_style : Ppx_hash_lib.Std.Hash.state -> case_style -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_case_style : case_style -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_case_style : case_style -> case_style -> int
Sourcetype case_printing = Constr.case_printing
Sourceval case_printing_of_sexp : Sexplib.Sexp.t -> case_printing
Sourceval sexp_of_case_printing : case_printing -> Sexplib.Sexp.t
Sourcetype case_info = Constr.case_info
Sourceval case_info_of_sexp : Sexplib.Sexp.t -> case_info
Sourceval sexp_of_case_info : case_info -> Sexplib.Sexp.t
Sourcetype rec_declaration = Constr.rec_declaration
Sourceval rec_declaration_of_sexp : Sexplib.Sexp.t -> rec_declaration
Sourceval sexp_of_rec_declaration : rec_declaration -> Sexplib.Sexp.t
Sourcetype fixpoint = Constr.fixpoint
Sourceval fixpoint_of_sexp : Sexplib.Sexp.t -> fixpoint
Sourceval sexp_of_fixpoint : fixpoint -> Sexplib.Sexp.t
Sourcetype cofixpoint = Constr.cofixpoint
Sourceval cofixpoint_of_sexp : Sexplib.Sexp.t -> cofixpoint
Sourceval sexp_of_cofixpoint : cofixpoint -> Sexplib.Sexp.t
Sourcetype 'constr pexistential = 'constr Constr.pexistential
Sourceval sexp_of_pexistential : ('constr -> Sexplib0.Sexp.t) -> 'constr pexistential -> Sexplib0.Sexp.t
Sourceval pexistential_of_sexp : (Sexplib0.Sexp.t -> 'constr) -> Sexplib0.Sexp.t -> 'constr pexistential
Sourceval pexistential_to_yojson : ('constr -> Yojson.Safe.t) -> 'constr pexistential -> Yojson.Safe.t
Sourceval hash_fold_pexistential : (Ppx_hash_lib.Std.Hash.state -> 'constr -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'constr pexistential -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_pexistential : ('constr -> 'constr -> int) -> 'constr pexistential -> 'constr pexistential -> int
Sourcetype ('constr, 'types, 'r) prec_declaration = ('constr, 'types, 'r) Constr.prec_declaration
Sourceval prec_declaration_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> (Sexplib.Sexp.t -> 'r) -> Sexplib.Sexp.t -> ('constr, 'types, 'r) prec_declaration
Sourceval sexp_of_prec_declaration : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('r -> Sexplib.Sexp.t) -> ('constr, 'types, 'r) prec_declaration -> Sexplib.Sexp.t
Sourcetype ('constr, 'types, 'r) pfixpoint = ('constr, 'types, 'r) Constr.pfixpoint
Sourceval pfixpoint_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> (Sexplib.Sexp.t -> 'r) -> Sexplib.Sexp.t -> ('constr, 'types, 'r) pfixpoint
Sourceval sexp_of_pfixpoint : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('r -> Sexplib.Sexp.t) -> ('constr, 'types, 'r) pfixpoint -> Sexplib.Sexp.t
Sourcetype ('constr, 'types, 'r) pcofixpoint = ('constr, 'types, 'r) Constr.pcofixpoint
Sourceval pcofixpoint_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> (Sexplib.Sexp.t -> 'r) -> Sexplib.Sexp.t -> ('constr, 'types, 'r) pcofixpoint
Sourceval sexp_of_pcofixpoint : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('r -> Sexplib.Sexp.t) -> ('constr, 'types, 'r) pcofixpoint -> Sexplib.Sexp.t
Sourcetype t = Constr.t
include Sexplib0.Sexpable.S with type t := t
Sourceval t_of_sexp : Sexplib0.Sexp.t -> t
Sourceval sexp_of_t : t -> Sexplib0.Sexp.t
Sourceval to_yojson : t -> Yojson.Safe.t
include Ppx_hash_lib.Hashable.S with type t := t
Sourceval hash_fold_t : t Base__Ppx_hash_lib.hash_fold
Sourceval hash : t -> Base__Ppx_hash_lib.Std.Hash.hash_value
include Ppx_compare_lib.Comparable.S with type t := t
Sourceval compare : t Base__Ppx_compare_lib.compare
Sourcetype constr = t
Sourceval sexp_of_constr : constr -> Sexplib0.Sexp.t
Sourceval constr_of_sexp : Sexplib0.Sexp.t -> constr
Sourceval constr_to_yojson : constr -> Yojson.Safe.t
Sourceval hash_fold_constr : Ppx_hash_lib.Std.Hash.state -> constr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_constr : constr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_constr : constr -> constr -> int
Sourcetype types = constr
Sourceval sexp_of_types : types -> Sexplib0.Sexp.t
Sourceval types_of_sexp : Sexplib0.Sexp.t -> types
Sourceval types_to_yojson : types -> Yojson.Safe.t
Sourceval hash_fold_types : Ppx_hash_lib.Std.Hash.state -> types -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_types : types -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_types : types -> types -> int
Sourcetype existential = Constr.existential
Sourceval existential_of_sexp : Sexplib.Sexp.t -> existential
Sourceval sexp_of_existential : existential -> Sexplib.Sexp.t
Sourcetype sorts_family = Sorts.family
Sourceval sorts_family_of_sexp : Sexplib.Sexp.t -> sorts_family
Sourceval sexp_of_sorts_family : sorts_family -> Sexplib.Sexp.t
Sourcetype named_declaration = Constr.named_declaration
Sourceval named_declaration_of_sexp : Sexplib.Sexp.t -> named_declaration
Sourceval sexp_of_named_declaration : named_declaration -> Sexplib.Sexp.t
Sourcetype named_context = Constr.named_context
Sourceval sexp_of_named_context : named_context -> Sexplib0.Sexp.t
Sourceval named_context_of_sexp : Sexplib0.Sexp.t -> named_context
Sourceval named_context_to_yojson : named_context -> Yojson.Safe.t
Sourceval hash_fold_named_context : Ppx_hash_lib.Std.Hash.state -> named_context -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_named_context : named_context -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_named_context : named_context -> named_context -> int
Sourcetype rel_declaration = Constr.rel_declaration
Sourceval rel_declaration_of_sexp : Sexplib.Sexp.t -> rel_declaration
Sourceval sexp_of_rel_declaration : rel_declaration -> Sexplib.Sexp.t
Sourcetype rel_context = Constr.rel_context
Sourceval sexp_of_rel_context : rel_context -> Sexplib0.Sexp.t
Sourceval rel_context_of_sexp : Sexplib0.Sexp.t -> rel_context
Sourceval rel_context_to_yojson : rel_context -> Yojson.Safe.t
Sourceval hash_fold_rel_context : Ppx_hash_lib.Std.Hash.state -> rel_context -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_rel_context : rel_context -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_rel_context : rel_context -> rel_context -> int