package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.15.0.0.15.3.tbz
sha256=8eb6117bccd54843b5553562f8925f8dc24f502e323479b4eb6e7e28265c8fda
sha512=049e071e43eaa418b37cbc6222fb9244ce50f136084cbfd96ee0c545f1d031f57dc72a2de8a6da08225194bc851ec1c51eaf5d1f1299b5003d78f4a4ef5ea4d9

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

Module Serlib.Ser_constrSource

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
Sourceval 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
Sourceval 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
Sourceval sexp_of_pexistential : ('constr -> Sexplib0.Sexp.t) -> 'constr pexistential -> Sexplib0.Sexp.t
Sourceval pexistential_of_sexp : (Sexplib0.Sexp.t -> 'constr) -> Sexplib0.Sexp.t -> 'constr pexistential
Sourceval pexistential_to_yojson : ('constr -> Yojson.Safe.t) -> 'constr pexistential -> Yojson.Safe.t
Sourceval 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
Sourceval compare_pexistential : ('constr -> 'constr -> int) -> 'constr pexistential -> 'constr pexistential -> int
Sourcetype ('constr, 'types) prec_declaration = ('constr, 'types) Constr.prec_declaration
Sourceval prec_declaration_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> Sexplib.Sexp.t -> ('constr, 'types) prec_declaration
Sourceval 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
Sourceval pfixpoint_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> Sexplib.Sexp.t -> ('constr, 'types) pfixpoint
Sourceval 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
Sourceval pcofixpoint_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'types) -> Sexplib.Sexp.t -> ('constr, 'types) pcofixpoint
Sourceval 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
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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
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