Module `Serlib.Ser_constr`Source

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

Source

val cast_kind_of_yojson : 
  Yojson.Safe.t ->
  cast_kind Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val case_style_of_yojson : 
  Yojson.Safe.t ->
  case_style Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val sexp_of_pexistential : 
  ('constr -> Sexplib0.Sexp.t) ->
  'constr pexistential ->
  Sexplib0.Sexp.t

Source

val pexistential_of_sexp : 
  (Sexplib0.Sexp.t -> 'constr) ->
  Sexplib0.Sexp.t ->
  'constr pexistential

Source

val pexistential_to_yojson : 
  ('constr -> Yojson.Safe.t) ->
  'constr pexistential ->
  Yojson.Safe.t

Source

val pexistential_of_yojson : 
  (Yojson.Safe.t -> 'constr Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'constr pexistential Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val compare_pexistential : 
  ('constr -> 'constr -> int) ->
  'constr pexistential ->
  'constr pexistential ->
  int

Source

type ('constr, 'types) prec_declaration =
  ('constr, 'types) Constr.prec_declaration

Source

val prec_declaration_of_sexp : 
  (Sexplib.Sexp.t -> 'constr) ->
  (Sexplib.Sexp.t -> 'types) ->
  Sexplib.Sexp.t ->
  ('constr, 'types) prec_declaration

Source

val sexp_of_prec_declaration : 
  ('constr -> Sexplib.Sexp.t) ->
  ('types -> Sexplib.Sexp.t) ->
  ('constr, 'types) prec_declaration ->
  Sexplib.Sexp.t

Sourcetype ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint

Source

val pfixpoint_of_sexp : 
  (Sexplib.Sexp.t -> 'constr) ->
  (Sexplib.Sexp.t -> 'types) ->
  Sexplib.Sexp.t ->
  ('constr, 'types) pfixpoint

Source

val sexp_of_pfixpoint : 
  ('constr -> Sexplib.Sexp.t) ->
  ('types -> Sexplib.Sexp.t) ->
  ('constr, 'types) pfixpoint ->
  Sexplib.Sexp.t

Sourcetype ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint

Source

val pcofixpoint_of_sexp : 
  (Sexplib.Sexp.t -> 'constr) ->
  (Sexplib.Sexp.t -> 'types) ->
  Sexplib.Sexp.t ->
  ('constr, 'types) pcofixpoint

Source

val sexp_of_pcofixpoint : 
  ('constr -> Sexplib.Sexp.t) ->
  ('types -> Sexplib.Sexp.t) ->
  ('constr, 'types) 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

Sourceval of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

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

Source

val constr_of_yojson : 
  Yojson.Safe.t ->
  constr Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val types_of_yojson : 
  Yojson.Safe.t ->
  types Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val named_context_of_yojson : 
  Yojson.Safe.t ->
  named_context Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val rel_context_of_yojson : 
  Yojson.Safe.t ->
  rel_context Ppx_deriving_yojson_runtime.error_or

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Serlib.Ser_constr`Source

package coq-serapi

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Serlib.Ser_constrSource

Module `Serlib.Ser_constr`Source