package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.10.0.0.7.2.tbz
sha256=39018932b0520cc042246a3f9e03f3788d1aaff65568b480d8681cba235032e9
sha512=62a3bb3950e5f9d9cfa5fca85a1108a04fd8c1833cba560ff9d52246ef96d3d61a4743e6dc6d52f53c6a495040fad53f1d9aae383609227a6eb84568ad2a1a6c
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 : constant_body -> Sexplib.Sexp.tval constant_body_of_sexp : Sexplib.Sexp.t -> 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