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_constr/index.html
Module Serlib.Ser_constr
val metavariable_of_sexp : Sexplib.Sexp.t -> metavariableval sexp_of_metavariable : metavariable -> Sexplib.Sexp.tval 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