Module `Serlib.Ser_decls`Source

Sourcetype definition_object_kind = Decls.definition_object_kind =

| Definition
| Coercion
| SubClass
| CanonicalStructure
| Example
| Fixpoint
| CoFixpoint
| Scheme
| StructureComponent
| IdentityCoercion
| Instance
| Method
| Let

Sourceval definition_object_kind_of_sexp : Sexplib0.Sexp.t -> definition_object_kind

Sourceval sexp_of_definition_object_kind : definition_object_kind -> Sexplib0.Sexp.t

Sourceval definition_object_kind_to_yojson : definition_object_kind -> Yojson.Safe.t

val definition_object_kind_of_yojson : 
  Yojson.Safe.t ->
  definition_object_kind Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_definition_object_kind : 
  Ppx_hash_lib.Std.Hash.state ->
  definition_object_kind ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_definition_object_kind : 
  definition_object_kind ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_definition_object_kind : 
  definition_object_kind ->
  definition_object_kind ->
  int

Sourcetype theorem_kind = Decls.theorem_kind =

| Theorem
| Lemma
| Fact
| Remark
| Property
| Proposition
| Corollary

Sourceval theorem_kind_of_sexp : Sexplib0.Sexp.t -> theorem_kind

Sourceval sexp_of_theorem_kind : theorem_kind -> Sexplib0.Sexp.t

Sourceval theorem_kind_to_yojson : theorem_kind -> Yojson.Safe.t

Source

val theorem_kind_of_yojson : 
  Yojson.Safe.t ->
  theorem_kind Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_theorem_kind : 
  Ppx_hash_lib.Std.Hash.state ->
  theorem_kind ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_theorem_kind : theorem_kind -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_theorem_kind : theorem_kind -> theorem_kind -> int

Sourcetype assumption_object_kind = Decls.assumption_object_kind =

| Definitional
| Logical
| Conjectural
| Context

Sourceval assumption_object_kind_of_sexp : Sexplib0.Sexp.t -> assumption_object_kind

Sourceval sexp_of_assumption_object_kind : assumption_object_kind -> Sexplib0.Sexp.t

Sourceval assumption_object_kind_to_yojson : assumption_object_kind -> Yojson.Safe.t

Source

val assumption_object_kind_of_yojson : 
  Yojson.Safe.t ->
  assumption_object_kind Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_assumption_object_kind : 
  Ppx_hash_lib.Std.Hash.state ->
  assumption_object_kind ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_assumption_object_kind : 
  assumption_object_kind ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_assumption_object_kind : 
  assumption_object_kind ->
  assumption_object_kind ->
  int

Sourcetype logical_kind = Decls.logical_kind =

| IsPrimitive
| IsAssumption of assumption_object_kind
| IsDefinition of definition_object_kind
| IsProof of theorem_kind

Sourceval logical_kind_of_sexp : Sexplib0.Sexp.t -> logical_kind

Sourceval sexp_of_logical_kind : logical_kind -> Sexplib0.Sexp.t

Sourceval logical_kind_to_yojson : logical_kind -> Yojson.Safe.t

Source

val logical_kind_of_yojson : 
  Yojson.Safe.t ->
  logical_kind Ppx_deriving_yojson_runtime.error_or

Sourceval _ : Yojson.Safe.t -> logical_kind Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_logical_kind : 
  Ppx_hash_lib.Std.Hash.state ->
  logical_kind ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_logical_kind : logical_kind -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_logical_kind : logical_kind -> logical_kind -> int

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-serapi.serlib/Serlib/Ser_decls/index.html

Module `Serlib.Ser_decls`Source

package coq-serapi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-serapi.serlib/Serlib/Ser_decls/index.html

Module Serlib.Ser_declsSource

Module `Serlib.Ser_decls`Source