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_decl_kinds/index.html
Module Serlib.Ser_decl_kinds
val locality_of_sexp : Sexplib.Sexp.t -> localityval sexp_of_locality : locality -> Sexplib.Sexp.tval binding_kind_of_sexp : Sexplib.Sexp.t -> binding_kindval sexp_of_binding_kind : binding_kind -> Sexplib.Sexp.tval binding_kind_of_yojson :
Yojson.Safe.t ->
(binding_kind, string) Result.resultval binding_kind_to_yojson : binding_kind -> Yojson.Safe.tval polymorphic_of_sexp : Sexplib.Sexp.t -> polymorphicval sexp_of_polymorphic : polymorphic -> Sexplib.Sexp.tval private_flag_of_sexp : Sexplib.Sexp.t -> private_flagval sexp_of_private_flag : private_flag -> Sexplib.Sexp.tval private_flag_of_yojson :
Yojson.Safe.t ->
(private_flag, string) Result.resultval private_flag_to_yojson : private_flag -> Yojson.Safe.tval cumulative_inductive_flag_of_sexp :
Sexplib.Sexp.t ->
cumulative_inductive_flagval sexp_of_cumulative_inductive_flag :
cumulative_inductive_flag ->
Sexplib.Sexp.tval theorem_kind_of_sexp : Sexplib.Sexp.t -> theorem_kindval sexp_of_theorem_kind : theorem_kind -> Sexplib.Sexp.tval theorem_kind_of_yojson :
Yojson.Safe.t ->
(theorem_kind, string) Result.resultval theorem_kind_to_yojson : theorem_kind -> Yojson.Safe.tval definition_object_kind_of_sexp : Sexplib.Sexp.t -> definition_object_kindval sexp_of_definition_object_kind : definition_object_kind -> Sexplib.Sexp.tval definition_object_kind_of_yojson :
Yojson.Safe.t ->
(definition_object_kind, string) Result.resultval definition_object_kind_to_yojson : definition_object_kind -> Yojson.Safe.tval assumption_object_kind_of_sexp : Sexplib.Sexp.t -> assumption_object_kindval sexp_of_assumption_object_kind : assumption_object_kind -> Sexplib.Sexp.tval assumption_object_kind_of_yojson :
Yojson.Safe.t ->
(assumption_object_kind, string) Result.resultval assumption_object_kind_to_yojson : assumption_object_kind -> Yojson.Safe.tval assumption_kind_of_sexp : Sexplib.Sexp.t -> assumption_kindval sexp_of_assumption_kind : assumption_kind -> Sexplib.Sexp.tval assumption_kind_of_yojson :
Yojson.Safe.t ->
(assumption_kind, string) Result.resultval assumption_kind_to_yojson : assumption_kind -> Yojson.Safe.tval definition_kind_of_sexp : Sexplib.Sexp.t -> definition_kindval sexp_of_definition_kind : definition_kind -> Sexplib.Sexp.tval goal_object_kind_of_sexp : Sexplib.Sexp.t -> goal_object_kindval sexp_of_goal_object_kind : goal_object_kind -> Sexplib.Sexp.tval goal_kind_of_sexp : Sexplib.Sexp.t -> goal_kindval sexp_of_goal_kind : goal_kind -> Sexplib.Sexp.tval logical_kind_of_sexp : Sexplib.Sexp.t -> logical_kindval sexp_of_logical_kind : logical_kind -> Sexplib.Sexp.tval discharge_of_sexp : Sexplib.Sexp.t -> dischargeval sexp_of_discharge : discharge -> Sexplib.Sexp.tval discharge_of_yojson : Yojson.Safe.t -> (discharge, string) Result.resultval discharge_to_yojson : discharge -> Yojson.Safe.t