package coq-serapi

  1. Overview
  2. Docs
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 cast_kind_to_yojson : cast_kind -> Yojson.Safe.t
val sexp_of_cast_kind : cast_kind -> Sexplib0.Sexp.t
val cast_kind_of_sexp : Sexplib0.Sexp.t -> cast_kind
val hash_fold_cast_kind : Base.Hash.state -> cast_kind -> Base.Hash.state
val hash_cast_kind : cast_kind -> Base.Hash.hash_value
val compare_cast_kind : cast_kind -> cast_kind -> int
type case_style = Constr.case_style
val case_style_to_yojson : case_style -> Yojson.Safe.t
val sexp_of_case_style : case_style -> Sexplib0.Sexp.t
val case_style_of_sexp : Sexplib0.Sexp.t -> case_style
val hash_fold_case_style : Base.Hash.state -> case_style -> Base.Hash.state
val hash_case_style : case_style -> Base.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 pexistential_to_yojson : ('constr -> Yojson.Safe.t) -> 'constr pexistential -> Yojson.Safe.t
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 hash_fold_pexistential : (Base.Hash.state -> 'constr -> Base.Hash.state) -> Base.Hash.state -> 'constr pexistential -> Base.Hash.state
val compare_pexistential : ('constr -> 'constr -> int) -> 'constr pexistential -> 'constr pexistential -> int
type ('constr, 'types) prec_declaration = ('constr, 'types) Constr.prec_declaration
val prec_declaration_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> Sexplib.Sexp.t -> ('constr, 'types) prec_declaration
val sexp_of_prec_declaration : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('constr, 'types) prec_declaration -> Sexplib.Sexp.t
type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
val pfixpoint_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> Sexplib.Sexp.t -> ('constr, 'types) pfixpoint
val sexp_of_pfixpoint : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('constr, 'types) pfixpoint -> Sexplib.Sexp.t
type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
val pcofixpoint_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> Sexplib.Sexp.t -> ('constr, 'types) pcofixpoint
val sexp_of_pcofixpoint : ('constr -> Sexplib.Sexp.t) -> ('types -> Sexplib.Sexp.t) -> ('constr, 'types) pcofixpoint -> Sexplib.Sexp.t
type t = Constr.t
val to_yojson : t -> Yojson.Safe.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
include Ppx_hash_lib.Hashable.S with type t := t
val hash_fold_t : Base.Hash.state -> t -> Base.Hash.state
val hash : t -> Base.Hash.hash_value
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t -> t -> int
type constr = t
val constr_to_yojson : constr -> Yojson.Safe.t
val sexp_of_constr : constr -> Sexplib0.Sexp.t
val constr_of_sexp : Sexplib0.Sexp.t -> constr
val hash_fold_constr : Base.Hash.state -> constr -> Base.Hash.state
val hash_constr : constr -> Base.Hash.hash_value
val compare_constr : constr -> constr -> int
type types = constr
val types_to_yojson : types -> Yojson.Safe.t
val sexp_of_types : types -> Sexplib0.Sexp.t
val types_of_sexp : Sexplib0.Sexp.t -> types
val hash_fold_types : Base.Hash.state -> types -> Base.Hash.state
val hash_types : types -> Base.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 named_context_to_yojson : named_context -> Yojson.Safe.t
val sexp_of_named_context : named_context -> Sexplib0.Sexp.t
val named_context_of_sexp : Sexplib0.Sexp.t -> named_context
val hash_fold_named_context : Base.Hash.state -> named_context -> Base.Hash.state
val hash_named_context : named_context -> Base.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 rel_context_to_yojson : rel_context -> Yojson.Safe.t
val sexp_of_rel_context : rel_context -> Sexplib0.Sexp.t
val rel_context_of_sexp : Sexplib0.Sexp.t -> rel_context
val hash_fold_rel_context : Base.Hash.state -> rel_context -> Base.Hash.state
val hash_rel_context : rel_context -> Base.Hash.hash_value
val compare_rel_context : rel_context -> rel_context -> int
OCaml

Innovation. Community. Security.