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.1.tbz
sha256=207b091d8d9d9e1a649759f0acfd15cbfda54a2627a01fc74aa74ec0ffaa3400
sha512=af85d00c5896e78a6edea7794070795ca14c8e47a0e9a28f2ac003364b0f99eb72f19f57e755a3967d255b1aaf62cae0d09bbab02d2d35ef6ee02b84823a0929
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