package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.12.0.0.12.1.tbz
sha256=08a12e8e8766c2e6a6a7394b0df48989c081367fa7d4d8dd8cdcd026575b4859
sha512=80267021f065f04543f72f16827fc7642ce98ed93940b0f780e83b0c751ac1a8df0e27018326315726c1b7b029015da31eec8322fda15a3a23c57850d53ef358
doc/coq-serapi.serlib/Serlib/Ser_declarations/index.html
Module Serlib.Ser_declarations
val template_arity_of_sexp : Sexplib.Sexp.t -> template_arityval sexp_of_template_arity : template_arity -> Sexplib.Sexp.tval declaration_arity_of_sexp :
(Sexplib.Sexp.t -> 'a) ->
(Sexplib.Sexp.t -> 'b) ->
Sexplib.Sexp.t ->
('a, 'b) declaration_arityval sexp_of_declaration_arity :
('a -> Sexplib.Sexp.t) ->
('b -> Sexplib.Sexp.t) ->
('a, 'b) declaration_arity ->
Sexplib.Sexp.tval recarg_of_sexp : Sexplib.Sexp.t -> recargval sexp_of_recarg : recarg -> Sexplib.Sexp.ttype wf_paths = recarg Rtree.tval wf_paths_of_sexp : Sexplib.Sexp.t -> wf_pathsval sexp_of_wf_paths : wf_paths -> Sexplib.Sexp.tval regular_inductive_arity_of_sexp : Sexplib.Sexp.t -> regular_inductive_arityval sexp_of_regular_inductive_arity : regular_inductive_arity -> Sexplib.Sexp.tval inductive_arity_of_sexp : Sexplib.Sexp.t -> inductive_arityval sexp_of_inductive_arity : inductive_arity -> Sexplib.Sexp.tval one_inductive_body_of_sexp : Sexplib.Sexp.t -> one_inductive_bodyval sexp_of_one_inductive_body : one_inductive_body -> Sexplib.Sexp.tval set_predicativity_of_sexp : Sexplib.Sexp.t -> set_predicativityval sexp_of_set_predicativity : set_predicativity -> Sexplib.Sexp.tval engagement_of_sexp : Sexplib.Sexp.t -> engagementval sexp_of_engagement : engagement -> Sexplib.Sexp.tval typing_flags_of_sexp : Sexplib.Sexp.t -> typing_flagsval sexp_of_typing_flags : typing_flags -> Sexplib.Sexp.tval sexp_of_inline : inline -> Sexplib.Sexp.tval inline_of_sexp : Sexplib.Sexp.t -> inlineval sexp_of_constant_body :
('opaque -> Sexplib.Sexp.t) ->
'opaque constant_body ->
Sexplib.Sexp.tval constant_body_of_sexp :
(Sexplib.Sexp.t -> 'opaque) ->
Sexplib.Sexp.t ->
'opaque constant_bodyval recursivity_kind_of_sexp : Sexplib.Sexp.t -> recursivity_kindval sexp_of_recursivity_kind : recursivity_kind -> Sexplib.Sexp.tval recursivity_kind_of_yojson :
Yojson.Safe.t ->
(recursivity_kind, string) Result.resultval recursivity_kind_to_yojson : recursivity_kind -> Yojson.Safe.tval mutual_inductive_body_of_sexp : Sexplib.Sexp.t -> mutual_inductive_bodyval sexp_of_mutual_inductive_body : mutual_inductive_body -> Sexplib.Sexp.tval sexp_of_module_alg_expr : module_alg_expr -> Sexplib.Sexp.tval module_alg_expr_of_sexp : Sexplib.Sexp.t -> module_alg_exprval sexp_of_structure_body : structure_body -> Sexplib.Sexp.tval structure_body_of_sexp : Sexplib.Sexp.t -> structure_bodyval sexp_of_module_body : module_body -> Sexplib.Sexp.tval module_body_of_sexp : Sexplib.Sexp.t -> module_bodyval sexp_of_module_type_body : module_type_body -> Sexplib.Sexp.tval module_type_body_of_sexp : Sexplib.Sexp.t -> module_type_body