package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
type metavariable = Constr.metavariable
val metavariable_of_sexp : Sexplib.Sexp.t -> metavariable
val sexp_of_metavariable : metavariable -> Sexplib.Sexp.t
type pconstant = Constr.pconstant
val pconstant_of_sexp : Sexplib.Sexp.t -> pconstant
val sexp_of_pconstant : pconstant -> Sexplib.Sexp.t
type pinductive = Constr.pinductive
val pinductive_of_sexp : Sexplib.Sexp.t -> pinductive
val sexp_of_pinductive : pinductive -> Sexplib.Sexp.t
type pconstructor = Constr.pconstructor
val pconstructor_of_sexp : Sexplib.Sexp.t -> pconstructor
val sexp_of_pconstructor : pconstructor -> Sexplib.Sexp.t
type cast_kind = Constr.cast_kind
val sexp_of_cast_kind : cast_kind -> Sexplib0.Sexp.t
val cast_kind_of_sexp : Sexplib0.Sexp.t -> cast_kind
val cast_kind_to_yojson : cast_kind -> Yojson.Safe.t
val cast_kind_of_yojson : Yojson.Safe.t -> cast_kind Ppx_deriving_yojson_runtime.error_or
val hash_fold_cast_kind : Ppx_hash_lib.Std.Hash.state -> cast_kind -> Ppx_hash_lib.Std.Hash.state
val hash_cast_kind : cast_kind -> Ppx_hash_lib.Std.Hash.hash_value
val compare_cast_kind : cast_kind -> cast_kind -> int
type case_style = Constr.case_style
val sexp_of_case_style : case_style -> Sexplib0.Sexp.t
val case_style_of_sexp : Sexplib0.Sexp.t -> case_style
val case_style_to_yojson : case_style -> Yojson.Safe.t
val case_style_of_yojson : Yojson.Safe.t -> case_style Ppx_deriving_yojson_runtime.error_or
val hash_fold_case_style : Ppx_hash_lib.Std.Hash.state -> case_style -> Ppx_hash_lib.Std.Hash.state
val hash_case_style : case_style -> Ppx_hash_lib.Std.Hash.hash_value
val compare_case_style : case_style -> case_style -> int
type case_printing = Constr.case_printing
val case_printing_of_sexp : Sexplib.Sexp.t -> case_printing
val sexp_of_case_printing : case_printing -> Sexplib.Sexp.t
type case_info = Constr.case_info
val case_info_of_sexp : Sexplib.Sexp.t -> case_info
val sexp_of_case_info : case_info -> Sexplib.Sexp.t
type rec_declaration = Constr.rec_declaration
val rec_declaration_of_sexp : Sexplib.Sexp.t -> rec_declaration
val sexp_of_rec_declaration : rec_declaration -> Sexplib.Sexp.t
type fixpoint = Constr.fixpoint
val fixpoint_of_sexp : Sexplib.Sexp.t -> fixpoint
val sexp_of_fixpoint : fixpoint -> Sexplib.Sexp.t
type cofixpoint = Constr.cofixpoint
val cofixpoint_of_sexp : Sexplib.Sexp.t -> cofixpoint
val sexp_of_cofixpoint : cofixpoint -> Sexplib.Sexp.t
type 'constr pexistential = 'constr Constr.pexistential
val sexp_of_pexistential : ('constr -> Sexplib0.Sexp.t) -> 'constr pexistential -> Sexplib0.Sexp.t
val pexistential_of_sexp : (Sexplib0.Sexp.t -> 'constr) -> Sexplib0.Sexp.t -> 'constr pexistential
val pexistential_to_yojson : ('constr -> Yojson.Safe.t) -> 'constr pexistential -> Yojson.Safe.t
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
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
val compare_pexistential : ('constr -> 'constr -> int) -> 'constr pexistential -> 'constr pexistential -> int
type ('constr, 'types, 'r) prec_declaration = ('constr, 'types, 'r) Constr.prec_declaration
val prec_declaration_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> (Sexplib.Sexp.t -> 'r) -> Sexplib.Sexp.t -> ('constr, 'types, 'r) prec_declaration
val sexp_of_prec_declaration : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('r -> Sexplib.Sexp.t) -> ('constr, 'types, 'r) prec_declaration -> Sexplib.Sexp.t
type ('constr, 'types, 'r) pfixpoint = ('constr, 'types, 'r) Constr.pfixpoint
val pfixpoint_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> (Sexplib.Sexp.t -> 'r) -> Sexplib.Sexp.t -> ('constr, 'types, 'r) pfixpoint
val sexp_of_pfixpoint : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('r -> Sexplib.Sexp.t) -> ('constr, 'types, 'r) pfixpoint -> Sexplib.Sexp.t
type ('constr, 'types, 'r) pcofixpoint = ('constr, 'types, 'r) Constr.pcofixpoint
val pcofixpoint_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> (Sexplib.Sexp.t -> 'r) -> Sexplib.Sexp.t -> ('constr, 'types, 'r) pcofixpoint
val sexp_of_pcofixpoint : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('r -> Sexplib.Sexp.t) -> ('constr, 'types, 'r) pcofixpoint -> Sexplib.Sexp.t
type t = Constr.t
include Sexplib0.Sexpable.S with type t := t
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_hash_lib.Hashable.S with type t := t
val hash_fold_t : t Base__Ppx_hash_lib.hash_fold
val hash : t -> Base__Ppx_hash_lib.Std.Hash.hash_value
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
type constr = t
val sexp_of_constr : constr -> Sexplib0.Sexp.t
val constr_of_sexp : Sexplib0.Sexp.t -> constr
val constr_to_yojson : constr -> Yojson.Safe.t
val constr_of_yojson : Yojson.Safe.t -> constr Ppx_deriving_yojson_runtime.error_or
val hash_fold_constr : Ppx_hash_lib.Std.Hash.state -> constr -> Ppx_hash_lib.Std.Hash.state
val hash_constr : constr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_constr : constr -> constr -> int
type types = constr
val sexp_of_types : types -> Sexplib0.Sexp.t
val types_of_sexp : Sexplib0.Sexp.t -> types
val types_to_yojson : types -> Yojson.Safe.t
val types_of_yojson : Yojson.Safe.t -> types Ppx_deriving_yojson_runtime.error_or
val hash_fold_types : Ppx_hash_lib.Std.Hash.state -> types -> Ppx_hash_lib.Std.Hash.state
val hash_types : types -> Ppx_hash_lib.Std.Hash.hash_value
val compare_types : types -> types -> int
type existential = Constr.existential
val existential_of_sexp : Sexplib.Sexp.t -> existential
val sexp_of_existential : existential -> Sexplib.Sexp.t
type sorts_family = Sorts.family
val sorts_family_of_sexp : Sexplib.Sexp.t -> sorts_family
val sexp_of_sorts_family : sorts_family -> Sexplib.Sexp.t
type named_declaration = Constr.named_declaration
val named_declaration_of_sexp : Sexplib.Sexp.t -> named_declaration
val sexp_of_named_declaration : named_declaration -> Sexplib.Sexp.t
type named_context = Constr.named_context
val sexp_of_named_context : named_context -> Sexplib0.Sexp.t
val named_context_of_sexp : Sexplib0.Sexp.t -> named_context
val named_context_to_yojson : named_context -> Yojson.Safe.t
val named_context_of_yojson : Yojson.Safe.t -> named_context Ppx_deriving_yojson_runtime.error_or
val hash_fold_named_context : Ppx_hash_lib.Std.Hash.state -> named_context -> Ppx_hash_lib.Std.Hash.state
val hash_named_context : named_context -> Ppx_hash_lib.Std.Hash.hash_value
val compare_named_context : named_context -> named_context -> int
type rel_declaration = Constr.rel_declaration
val rel_declaration_of_sexp : Sexplib.Sexp.t -> rel_declaration
val sexp_of_rel_declaration : rel_declaration -> Sexplib.Sexp.t
type rel_context = Constr.rel_context
val sexp_of_rel_context : rel_context -> Sexplib0.Sexp.t
val rel_context_of_sexp : Sexplib0.Sexp.t -> rel_context
val rel_context_to_yojson : rel_context -> Yojson.Safe.t
val rel_context_of_yojson : Yojson.Safe.t -> rel_context Ppx_deriving_yojson_runtime.error_or
val hash_fold_rel_context : Ppx_hash_lib.Std.Hash.state -> rel_context -> Ppx_hash_lib.Std.Hash.state
val hash_rel_context : rel_context -> Ppx_hash_lib.Std.Hash.hash_value
val compare_rel_context : rel_context -> rel_context -> 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