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 (35)

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.4.9.1.tbz
sha256=667908bdd88f0bb1b75d2fa76a483006d600c9422a2a15297a172e62c0415cad
sha512=42f8e5ad308702f77c9dc40243acd2e656b16bdb94c302306dbb87387cc36941deccd5f52c18d1a045467030ddf86528b22819522a647eee5b9e1ac25f4a9560

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

Module Serlib.Ser_genargSource

Sourcetype rlevel = Genarg.rlevel
Sourceval sexp_of_rlevel : rlevel -> Sexplib0.Sexp.t
Sourceval rlevel_of_sexp : Sexplib0.Sexp.t -> rlevel
Sourceval rlevel_to_yojson : rlevel -> Yojson.Safe.t
Sourceval hash_fold_rlevel : Ppx_hash_lib.Std.Hash.state -> rlevel -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_rlevel : rlevel -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_rlevel : rlevel -> rlevel -> int
Sourcetype glevel = Genarg.glevel
Sourceval sexp_of_glevel : glevel -> Sexplib0.Sexp.t
Sourceval glevel_of_sexp : Sexplib0.Sexp.t -> glevel
Sourceval glevel_to_yojson : glevel -> Yojson.Safe.t
Sourceval hash_fold_glevel : Ppx_hash_lib.Std.Hash.state -> glevel -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glevel : glevel -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glevel : glevel -> glevel -> int
Sourcetype tlevel = Genarg.tlevel
Sourceval sexp_of_tlevel : tlevel -> Sexplib0.Sexp.t
Sourceval tlevel_of_sexp : Sexplib0.Sexp.t -> tlevel
Sourceval tlevel_to_yojson : tlevel -> Yojson.Safe.t
Sourceval hash_fold_tlevel : Ppx_hash_lib.Std.Hash.state -> tlevel -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_tlevel : tlevel -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_tlevel : tlevel -> tlevel -> int
Sourcetype 'a generic_argument = 'a Genarg.generic_argument
Sourceval sexp_of_generic_argument : ('a -> Sexplib0.Sexp.t) -> 'a generic_argument -> Sexplib0.Sexp.t
Sourceval generic_argument_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a generic_argument
Sourceval generic_argument_to_yojson : ('a -> Yojson.Safe.t) -> 'a generic_argument -> Yojson.Safe.t
Sourceval hash_fold_generic_argument : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a generic_argument -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_generic_argument : ('a -> 'a -> int) -> 'a generic_argument -> 'a generic_argument -> int
Sourcetype glob_generic_argument = Genarg.glob_generic_argument
Sourceval sexp_of_glob_generic_argument : glob_generic_argument -> Sexplib0.Sexp.t
Sourceval glob_generic_argument_of_sexp : Sexplib0.Sexp.t -> glob_generic_argument
Sourceval glob_generic_argument_to_yojson : glob_generic_argument -> Yojson.Safe.t
Sourceval hash_fold_glob_generic_argument : Ppx_hash_lib.Std.Hash.state -> glob_generic_argument -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glob_generic_argument : glob_generic_argument -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glob_generic_argument : glob_generic_argument -> glob_generic_argument -> int
Sourcetype raw_generic_argument = Genarg.raw_generic_argument
Sourceval sexp_of_raw_generic_argument : raw_generic_argument -> Sexplib0.Sexp.t
Sourceval raw_generic_argument_of_sexp : Sexplib0.Sexp.t -> raw_generic_argument
Sourceval raw_generic_argument_to_yojson : raw_generic_argument -> Yojson.Safe.t
Sourceval hash_fold_raw_generic_argument : Ppx_hash_lib.Std.Hash.state -> raw_generic_argument -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_generic_argument : raw_generic_argument -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_generic_argument : raw_generic_argument -> raw_generic_argument -> int
Sourcetype typed_generic_argument = Genarg.typed_generic_argument
Sourceval typed_generic_argument_of_sexp : Sexplib.Sexp.t -> Genarg.typed_generic_argument
Sourceval sexp_of_typed_generic_argument : Genarg.typed_generic_argument -> Sexplib.Sexp.t
Sourcetype ('raw, 'glb, 'top) gen_ser = {
  1. raw_ser : 'raw -> Sexplib.Sexp.t;
  2. raw_des : Sexplib.Sexp.t -> 'raw;
  3. raw_hash : 'raw Ppx_hash_lib.Std.Hash.folder;
  4. raw_compare : 'raw -> 'raw -> int;
  5. glb_ser : 'glb -> Sexplib.Sexp.t;
  6. glb_des : Sexplib.Sexp.t -> 'glb;
  7. glb_hash : 'glb Ppx_hash_lib.Std.Hash.folder;
  8. glb_compare : 'glb -> 'glb -> int;
  9. top_ser : 'top -> Sexplib.Sexp.t;
  10. top_des : Sexplib.Sexp.t -> 'top;
  11. top_hash : 'top Ppx_hash_lib.Std.Hash.folder;
  12. top_compare : 'top -> 'top -> int;
}
Sourceval register_genser : ('raw, 'glb, 'top) Genarg.genarg_type -> ('raw, 'glb, 'top) gen_ser -> unit
Sourceval gen_ser_pair : ('raw1, 'glb1, 'top1) gen_ser -> ('raw2, 'glb2, 'top2) gen_ser -> ('raw1 * 'raw2, 'glb1 * 'glb2, 'top1 * 'top2) gen_ser
Sourceval gen_ser_list : ('raw, 'glb, 'top) gen_ser -> ('raw list, 'glb list, 'top list) gen_ser
Sourceval mk_uniform : ('t -> Sexplib.Sexp.t) -> (Sexplib.Sexp.t -> 't) -> 't Ppx_hash_lib.Std.Hash.folder -> 't Ppx_compare_lib.compare -> ('t, 't, 't) gen_ser
Sourceval mk_vernac_arg : ('t -> Sexplib.Sexp.t) -> (Sexplib.Sexp.t -> 't) -> 't Ppx_hash_lib.Std.Hash.folder -> 't Ppx_compare_lib.compare -> ('t, Util.Empty.t, Util.Empty.t) gen_ser
Sourcemodule type GenSer0 = sig ... end
Sourcemodule GS0 (M : GenSer0) : sig ... end
Sourcemodule GSV (M : GenSer0) : sig ... end
Sourcemodule type GenSer = sig ... end
Sourcemodule GS (M : GenSer) : sig ... end
Sourcemodule type RType = sig ... end

Rocq Ast Analyzers and Synthetizers

Sourcemodule Analyzer : sig ... end