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.18.0.0.18.1.tbz
sha256=3958ec27603e3f927a74f11d02d98390e8ecda942bb23f37ff6fa575b31a8158
sha512=d33f9340de6e1426a42192da3610a7636b0201baa166cf788926b866738ae299219439bc22112cc81591c565dd857f66e53a41a3cfe420844f31fb6077abe57b

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

Module Serlib.Ser_declarationsSource

Sourcetype template_arity = Declarations.template_arity
Sourceval template_arity_of_sexp : Sexplib.Sexp.t -> template_arity
Sourceval sexp_of_template_arity : template_arity -> Sexplib.Sexp.t
Sourcetype ('a, 'b) declaration_arity = ('a, 'b) Declarations.declaration_arity
Sourceval declaration_arity_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'b) -> Sexplib.Sexp.t -> ('a, 'b) declaration_arity
Sourceval sexp_of_declaration_arity : ('a -> Sexplib.Sexp.t) -> ('b -> Sexplib.Sexp.t) -> ('a, 'b) declaration_arity -> Sexplib.Sexp.t
Sourcetype recarg = Declarations.recarg
Sourceval sexp_of_recarg : recarg -> Sexplib0.Sexp.t
Sourceval recarg_of_sexp : Sexplib0.Sexp.t -> recarg
Sourceval recarg_to_yojson : recarg -> Yojson.Safe.t
Sourceval hash_fold_recarg : Ppx_hash_lib.Std.Hash.state -> recarg -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_recarg : recarg -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_recarg : recarg -> recarg -> int
Sourcetype wf_paths = recarg Rtree.t
Sourceval sexp_of_wf_paths : wf_paths -> Sexplib0.Sexp.t
Sourceval wf_paths_of_sexp : Sexplib0.Sexp.t -> wf_paths
Sourceval wf_paths_to_yojson : wf_paths -> Yojson.Safe.t
Sourceval hash_fold_wf_paths : Ppx_hash_lib.Std.Hash.state -> wf_paths -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_wf_paths : wf_paths -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_wf_paths : wf_paths -> wf_paths -> int
Sourcetype regular_inductive_arity = Declarations.regular_inductive_arity
Sourceval sexp_of_regular_inductive_arity : regular_inductive_arity -> Sexplib0.Sexp.t
Sourceval regular_inductive_arity_of_sexp : Sexplib0.Sexp.t -> regular_inductive_arity
Sourceval regular_inductive_arity_to_yojson : regular_inductive_arity -> Yojson.Safe.t
Sourceval hash_fold_regular_inductive_arity : Ppx_hash_lib.Std.Hash.state -> regular_inductive_arity -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_regular_inductive_arity : regular_inductive_arity -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_regular_inductive_arity : regular_inductive_arity -> regular_inductive_arity -> int
Sourcetype inductive_arity = Declarations.inductive_arity
Sourceval sexp_of_inductive_arity : inductive_arity -> Sexplib0.Sexp.t
Sourceval inductive_arity_of_sexp : Sexplib0.Sexp.t -> inductive_arity
Sourceval inductive_arity_to_yojson : inductive_arity -> Yojson.Safe.t
Sourceval hash_fold_inductive_arity : Ppx_hash_lib.Std.Hash.state -> inductive_arity -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_inductive_arity : inductive_arity -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_inductive_arity : inductive_arity -> inductive_arity -> int
Sourcetype one_inductive_body = Declarations.one_inductive_body
Sourceval sexp_of_one_inductive_body : one_inductive_body -> Sexplib0.Sexp.t
Sourceval one_inductive_body_of_sexp : Sexplib0.Sexp.t -> one_inductive_body
Sourceval one_inductive_body_to_yojson : one_inductive_body -> Yojson.Safe.t
Sourceval one_inductive_body_of_yojson : Yojson.Safe.t -> one_inductive_body Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_one_inductive_body : Ppx_hash_lib.Std.Hash.state -> one_inductive_body -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_one_inductive_body : one_inductive_body -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_one_inductive_body : one_inductive_body -> one_inductive_body -> int
Sourcetype typing_flags = Declarations.typing_flags
Sourceval sexp_of_typing_flags : typing_flags -> Sexplib0.Sexp.t
Sourceval typing_flags_of_sexp : Sexplib0.Sexp.t -> typing_flags
Sourceval typing_flags_to_yojson : typing_flags -> Yojson.Safe.t
Sourceval hash_fold_typing_flags : Ppx_hash_lib.Std.Hash.state -> typing_flags -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_typing_flags : typing_flags -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_typing_flags : typing_flags -> typing_flags -> int
Sourcetype inline = Declarations.inline
Sourceval sexp_of_inline : inline -> Sexplib0.Sexp.t
Sourceval inline_of_sexp : Sexplib0.Sexp.t -> inline
Sourceval inline_to_yojson : inline -> Yojson.Safe.t
Sourceval hash_fold_inline : Ppx_hash_lib.Std.Hash.state -> inline -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_inline : inline -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_inline : inline -> inline -> int
Sourcetype 'a pconstant_body = 'a Declarations.pconstant_body
Sourceval sexp_of_pconstant_body : ('a -> Sexplib0.Sexp.t) -> 'a pconstant_body -> Sexplib0.Sexp.t
Sourceval pconstant_body_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a pconstant_body
Sourceval pconstant_body_to_yojson : ('a -> Yojson.Safe.t) -> 'a pconstant_body -> Yojson.Safe.t
Sourceval pconstant_body_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a pconstant_body Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_pconstant_body : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a pconstant_body -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_pconstant_body : ('a -> 'a -> int) -> 'a pconstant_body -> 'a pconstant_body -> int
Sourcetype constant_body = Declarations.constant_body
Sourceval sexp_of_constant_body : constant_body -> Sexplib0.Sexp.t
Sourceval constant_body_of_sexp : Sexplib0.Sexp.t -> constant_body
Sourceval constant_body_to_yojson : constant_body -> Yojson.Safe.t
Sourceval constant_body_of_yojson : Yojson.Safe.t -> constant_body Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_constant_body : Ppx_hash_lib.Std.Hash.state -> constant_body -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_constant_body : constant_body -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_constant_body : constant_body -> constant_body -> int
Sourcetype recursivity_kind = Declarations.recursivity_kind
Sourceval sexp_of_recursivity_kind : recursivity_kind -> Sexplib0.Sexp.t
Sourceval recursivity_kind_of_sexp : Sexplib0.Sexp.t -> recursivity_kind
Sourceval recursivity_kind_to_yojson : recursivity_kind -> Yojson.Safe.t
Sourceval hash_fold_recursivity_kind : Ppx_hash_lib.Std.Hash.state -> recursivity_kind -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_recursivity_kind : recursivity_kind -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_recursivity_kind : recursivity_kind -> recursivity_kind -> int
Sourcetype mutual_inductive_body = Declarations.mutual_inductive_body
Sourceval sexp_of_mutual_inductive_body : mutual_inductive_body -> Sexplib0.Sexp.t
Sourceval mutual_inductive_body_of_sexp : Sexplib0.Sexp.t -> mutual_inductive_body
Sourceval mutual_inductive_body_to_yojson : mutual_inductive_body -> Yojson.Safe.t
Sourceval mutual_inductive_body_of_yojson : Yojson.Safe.t -> mutual_inductive_body Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_mutual_inductive_body : Ppx_hash_lib.Std.Hash.state -> mutual_inductive_body -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_mutual_inductive_body : mutual_inductive_body -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_mutual_inductive_body : mutual_inductive_body -> mutual_inductive_body -> int
Sourcetype 'a module_alg_expr = 'a Declarations.module_alg_expr
Sourceval sexp_of_module_alg_expr : ('a -> Sexplib0.Sexp.t) -> 'a module_alg_expr -> Sexplib0.Sexp.t
Sourceval module_alg_expr_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a module_alg_expr
Sourceval module_alg_expr_to_yojson : ('a -> Yojson.Safe.t) -> 'a module_alg_expr -> Yojson.Safe.t
Sourceval hash_fold_module_alg_expr : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a module_alg_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_module_alg_expr : ('a -> 'a -> int) -> 'a module_alg_expr -> 'a module_alg_expr -> int
Sourcetype structure_body = Declarations.structure_body
Sourceval sexp_of_structure_body : structure_body -> Sexplib0.Sexp.t
Sourceval structure_body_of_sexp : Sexplib0.Sexp.t -> structure_body
Sourceval structure_body_to_yojson : structure_body -> Yojson.Safe.t
Sourceval structure_body_of_yojson : Yojson.Safe.t -> structure_body Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_structure_body : Ppx_hash_lib.Std.Hash.state -> structure_body -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_structure_body : structure_body -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_structure_body : structure_body -> structure_body -> int
Sourcetype module_body = Declarations.module_body
Sourceval sexp_of_module_body : module_body -> Sexplib0.Sexp.t
Sourceval module_body_of_sexp : Sexplib0.Sexp.t -> module_body
Sourceval module_body_to_yojson : module_body -> Yojson.Safe.t
Sourceval module_body_of_yojson : Yojson.Safe.t -> module_body Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_module_body : Ppx_hash_lib.Std.Hash.state -> module_body -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_module_body : module_body -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_module_body : module_body -> module_body -> int
Sourcetype module_type_body = Declarations.module_type_body
Sourceval sexp_of_module_type_body : module_type_body -> Sexplib0.Sexp.t
Sourceval module_type_body_of_sexp : Sexplib0.Sexp.t -> module_type_body
Sourceval module_type_body_to_yojson : module_type_body -> Yojson.Safe.t
Sourceval module_type_body_of_yojson : Yojson.Safe.t -> module_type_body Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_module_type_body : Ppx_hash_lib.Std.Hash.state -> module_type_body -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_module_type_body : module_type_body -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_module_type_body : module_type_body -> module_type_body -> 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