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_constr/index.html
Module Serlib.Ser_constr
val pconstant_of_sexp : Sexplib.Sexp.t -> pconstantval sexp_of_pconstant : pconstant -> Sexplib.Sexp.tval pinductive_of_sexp : Sexplib.Sexp.t -> pinductiveval sexp_of_pinductive : pinductive -> Sexplib.Sexp.tval pconstructor_of_sexp : Sexplib.Sexp.t -> pconstructorval sexp_of_pconstructor : pconstructor -> Sexplib.Sexp.tval cast_kind_of_sexp : Sexplib.Sexp.t -> cast_kindval sexp_of_cast_kind : cast_kind -> Sexplib.Sexp.tval case_style_of_sexp : Sexplib.Sexp.t -> case_styleval sexp_of_case_style : case_style -> Sexplib.Sexp.tval case_style_of_yojson : Yojson.Safe.t -> (case_style, string) Result.resultval case_style_to_yojson : case_style -> Yojson.Safe.tval case_printing_of_sexp : Sexplib.Sexp.t -> case_printingval sexp_of_case_printing : case_printing -> Sexplib.Sexp.tval case_info_of_sexp : Sexplib.Sexp.t -> case_infoval sexp_of_case_info : case_info -> Sexplib.Sexp.tval rec_declaration_of_sexp : Sexplib.Sexp.t -> rec_declarationval sexp_of_rec_declaration : rec_declaration -> Sexplib.Sexp.tval fixpoint_of_sexp : Sexplib.Sexp.t -> fixpointval sexp_of_fixpoint : fixpoint -> Sexplib.Sexp.tval cofixpoint_of_sexp : Sexplib.Sexp.t -> cofixpointval sexp_of_cofixpoint : cofixpoint -> Sexplib.Sexp.tval pexistential_of_sexp :
(Sexplib.Sexp.t -> 'constr) ->
Sexplib.Sexp.t ->
'constr pexistentialval sexp_of_pexistential :
('constr -> Sexplib.Sexp.t) ->
'constr pexistential ->
Sexplib.Sexp.tval prec_declaration_of_sexp :
(Sexplib.Sexp.t -> 'constr) ->
(Sexplib.Sexp.t -> 'types) ->
Sexplib.Sexp.t ->
('constr, 'types) prec_declarationval sexp_of_prec_declaration :
('constr -> Sexplib.Sexp.t) ->
('types -> Sexplib.Sexp.t) ->
('constr, 'types) prec_declaration ->
Sexplib.Sexp.tval pfixpoint_of_sexp :
(Sexplib.Sexp.t -> 'constr) ->
(Sexplib.Sexp.t -> 'types) ->
Sexplib.Sexp.t ->
('constr, 'types) pfixpointval sexp_of_pfixpoint :
('constr -> Sexplib.Sexp.t) ->
('types -> Sexplib.Sexp.t) ->
('constr, 'types) pfixpoint ->
Sexplib.Sexp.tval pcofixpoint_of_sexp :
(Sexplib.Sexp.t -> 'constr) ->
(Sexplib.Sexp.t -> 'types) ->
Sexplib.Sexp.t ->
('constr, 'types) pcofixpointval sexp_of_pcofixpoint :
('constr -> Sexplib.Sexp.t) ->
('types -> Sexplib.Sexp.t) ->
('constr, 'types) pcofixpoint ->
Sexplib.Sexp.tval t_of_sexp : Sexplib.Sexp.t -> tval sexp_of_t : t -> Sexplib.Sexp.tval of_yojson : Yojson.Safe.t -> (t, string) Result.resultval to_yojson : t -> Yojson.Safe.ttype constr = tval constr_of_sexp : Sexplib.Sexp.t -> constrval sexp_of_constr : constr -> Sexplib.Sexp.tval constr_of_yojson : Yojson.Safe.t -> (constr, string) Result.resultval constr_to_yojson : constr -> Yojson.Safe.ttype types = constrval types_of_sexp : Sexplib.Sexp.t -> typesval sexp_of_types : types -> Sexplib.Sexp.tval types_of_yojson : Yojson.Safe.t -> (types, string) Result.resultval types_to_yojson : types -> Yojson.Safe.tval existential_of_sexp : Sexplib.Sexp.t -> existentialval sexp_of_existential : existential -> Sexplib.Sexp.tval sorts_family_of_sexp : Sexplib.Sexp.t -> sorts_familyval sexp_of_sorts_family : sorts_family -> Sexplib.Sexp.tval named_declaration_of_sexp : Sexplib.Sexp.t -> named_declarationval sexp_of_named_declaration : named_declaration -> Sexplib.Sexp.tval named_context_of_sexp : Sexplib.Sexp.t -> named_contextval sexp_of_named_context : named_context -> Sexplib.Sexp.tval rel_declaration_of_sexp : Sexplib.Sexp.t -> rel_declarationval sexp_of_rel_declaration : rel_declaration -> Sexplib.Sexp.tval rel_context_of_sexp : Sexplib.Sexp.t -> rel_contextval sexp_of_rel_context : rel_context -> Sexplib.Sexp.t