package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.11.0+0.11.1.tbz
sha256=f06bb0ab1041ac6f8d73faddda404827ce94b6b3310483e93d7fd18bd018e1ed
sha512=ecbed7b5b8451f65d40bf50fd1471b5038029c6f1ae8912c8cb51e61699cc4c158bc4f3533ec5f0898d1fc3d91683c0ff815fa44be7fdaedea59b71ca1d1b7d3
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