package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Serlib.Ser_declsSource

Sourcetype 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
Sourceval definition_object_kind_to_yojson : definition_object_kind -> Yojson.Safe.t
Sourceval definition_object_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> definition_object_kind
Sourceval sexp_of_definition_object_kind : definition_object_kind -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype theorem_kind = Decls.theorem_kind =
  1. | Theorem
  2. | Lemma
  3. | Fact
  4. | Remark
  5. | Property
  6. | Proposition
  7. | Corollary
Sourceval theorem_kind_to_yojson : theorem_kind -> Yojson.Safe.t
Sourceval theorem_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> theorem_kind
Sourceval sexp_of_theorem_kind : theorem_kind -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype assumption_object_kind = Decls.assumption_object_kind =
  1. | Definitional
  2. | Logical
  3. | Conjectural
  4. | Context
Sourceval assumption_object_kind_to_yojson : assumption_object_kind -> Yojson.Safe.t
Sourceval assumption_object_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> assumption_object_kind
Sourceval sexp_of_assumption_object_kind : assumption_object_kind -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype logical_kind = Decls.logical_kind =
  1. | IsPrimitive
  2. | IsAssumption of assumption_object_kind
  3. | IsDefinition of definition_object_kind
  4. | IsProof of theorem_kind
Sourceval logical_kind_to_yojson : logical_kind -> Yojson.Safe.t
Sourceval _ : Yojson.Safe.t -> logical_kind Ppx_deriving_yojson_runtime.error_or
Sourceval logical_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> logical_kind
Sourceval sexp_of_logical_kind : logical_kind -> Ppx_sexp_conv_lib.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