package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
type definition_object_kind = Decls.definition_object_kind =
  1. | Definition
  2. | Coercion
  3. | SubClass
  4. | CanonicalStructure
  5. | Example
  6. | Fixpoint
  7. | CoFixpoint
  8. | Scheme
  9. | StructureComponent
  10. | IdentityCoercion
  11. | Instance
  12. | Method
  13. | Let
  14. | LetContext
val definition_object_kind_of_sexp : Sexplib0.Sexp.t -> definition_object_kind
val sexp_of_definition_object_kind : definition_object_kind -> Sexplib0.Sexp.t
val definition_object_kind_to_yojson : definition_object_kind -> Yojson.Safe.t
val hash_fold_definition_object_kind : Base.Hash.state -> definition_object_kind -> Base.Hash.state
val hash_definition_object_kind : definition_object_kind -> Base.Hash.hash_value
val compare_definition_object_kind : definition_object_kind -> definition_object_kind -> int
type theorem_kind = Decls.theorem_kind =
  1. | Theorem
  2. | Lemma
  3. | Fact
  4. | Remark
  5. | Property
  6. | Proposition
  7. | Corollary
val theorem_kind_of_sexp : Sexplib0.Sexp.t -> theorem_kind
val sexp_of_theorem_kind : theorem_kind -> Sexplib0.Sexp.t
val theorem_kind_to_yojson : theorem_kind -> Yojson.Safe.t
val hash_fold_theorem_kind : Base.Hash.state -> theorem_kind -> Base.Hash.state
val hash_theorem_kind : theorem_kind -> Base.Hash.hash_value
val compare_theorem_kind : theorem_kind -> theorem_kind -> int
type assumption_object_kind = Decls.assumption_object_kind =
  1. | Definitional
  2. | Logical
  3. | Conjectural
  4. | Context
val assumption_object_kind_of_sexp : Sexplib0.Sexp.t -> assumption_object_kind
val sexp_of_assumption_object_kind : assumption_object_kind -> Sexplib0.Sexp.t
val assumption_object_kind_to_yojson : assumption_object_kind -> Yojson.Safe.t
val hash_fold_assumption_object_kind : Base.Hash.state -> assumption_object_kind -> Base.Hash.state
val hash_assumption_object_kind : assumption_object_kind -> Base.Hash.hash_value
val compare_assumption_object_kind : assumption_object_kind -> assumption_object_kind -> int
type logical_kind = Decls.logical_kind =
  1. | IsPrimitive
  2. | IsSymbol
  3. | IsAssumption of assumption_object_kind
  4. | IsDefinition of definition_object_kind
  5. | IsProof of theorem_kind
val logical_kind_of_sexp : Sexplib0.Sexp.t -> logical_kind
val sexp_of_logical_kind : logical_kind -> Sexplib0.Sexp.t
val logical_kind_to_yojson : logical_kind -> Yojson.Safe.t
val _ : Yojson.Safe.t -> logical_kind Ppx_deriving_yojson_runtime.error_or
val hash_fold_logical_kind : Base.Hash.state -> logical_kind -> Base.Hash.state
val hash_logical_kind : logical_kind -> Base.Hash.hash_value
val compare_logical_kind : logical_kind -> logical_kind -> int
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