package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-serapi-8.11.0.0.11.0.tbz
sha256=59d38d716fda7cb1d89e2e1519c93d22deaf14da4f0f2feccd45886317f3424c
sha512=21b0ccaf75b497e13662c3fa2c618413dfccf6abfaabbab1d27926836447a0fcdc0e2a92929401359321018a4a867124caad27e9db52c4f3e5040aff698999ef
doc/coq-serapi.serlib/Serlib/Ser_vernacexpr/index.html
Module Serlib.Ser_vernacexpr
val class_rawexpr_of_sexp : Sexplib.Sexp.t -> class_rawexprval sexp_of_class_rawexpr : class_rawexpr -> Sexplib.Sexp.tval goal_identifier_of_sexp : Sexplib.Sexp.t -> goal_identifierval sexp_of_goal_identifier : goal_identifier -> Sexplib.Sexp.tval scope_name_of_sexp : Sexplib.Sexp.t -> scope_nameval sexp_of_scope_name : scope_name -> Sexplib.Sexp.tval goal_reference_of_sexp : Sexplib.Sexp.t -> goal_referenceval sexp_of_goal_reference : goal_reference -> Sexplib.Sexp.tval printable_of_sexp : Sexplib.Sexp.t -> printableval sexp_of_printable : printable -> Sexplib.Sexp.tval search_about_item_of_sexp : Sexplib.Sexp.t -> search_about_itemval sexp_of_search_about_item : search_about_item -> Sexplib.Sexp.tval searchable_of_sexp : Sexplib.Sexp.t -> searchableval sexp_of_searchable : searchable -> Sexplib.Sexp.tval locatable_of_sexp : Sexplib.Sexp.t -> locatableval sexp_of_locatable : locatable -> Sexplib.Sexp.tval showable_of_sexp : Sexplib.Sexp.t -> showableval sexp_of_showable : showable -> Sexplib.Sexp.tval comment_of_sexp : Sexplib.Sexp.t -> commentval sexp_of_comment : comment -> Sexplib.Sexp.tval search_restriction_of_sexp : Sexplib.Sexp.t -> search_restrictionval sexp_of_search_restriction : search_restriction -> Sexplib.Sexp.tval rec_flag_of_sexp : Sexplib.Sexp.t -> rec_flagval sexp_of_rec_flag : rec_flag -> Sexplib.Sexp.tval verbose_flag_of_sexp : Sexplib.Sexp.t -> verbose_flagval sexp_of_verbose_flag : verbose_flag -> Sexplib.Sexp.tval coercion_flag_of_sexp : Sexplib.Sexp.t -> coercion_flagval sexp_of_coercion_flag : coercion_flag -> Sexplib.Sexp.tval inductive_flag_of_sexp : Sexplib.Sexp.t -> inductive_flagval sexp_of_inductive_flag : inductive_flag -> Sexplib.Sexp.tval instance_flag_of_sexp : Sexplib.Sexp.t -> instance_flagval sexp_of_instance_flag : instance_flag -> Sexplib.Sexp.tval export_flag_of_sexp : Sexplib.Sexp.t -> export_flagval sexp_of_export_flag : export_flag -> Sexplib.Sexp.tval onlyparsing_flag_of_sexp : Sexplib.Sexp.t -> onlyparsing_flagval sexp_of_onlyparsing_flag : onlyparsing_flag -> Sexplib.Sexp.tval locality_flag_of_sexp : Sexplib.Sexp.t -> locality_flagval sexp_of_locality_flag : locality_flag -> Sexplib.Sexp.tval option_ref_value_of_sexp : Sexplib.Sexp.t -> option_ref_valueval sexp_of_option_ref_value : option_ref_value -> Sexplib.Sexp.tval sort_expr_of_sexp : Sexplib.Sexp.t -> sort_exprval sexp_of_sort_expr : sort_expr -> Sexplib.Sexp.tval definition_expr_of_sexp : Sexplib.Sexp.t -> definition_exprval sexp_of_definition_expr : definition_expr -> Sexplib.Sexp.tval fixpoint_expr_of_sexp : Sexplib.Sexp.t -> fixpoint_exprval sexp_of_fixpoint_expr : fixpoint_expr -> Sexplib.Sexp.tval cofixpoint_expr_of_sexp : Sexplib.Sexp.t -> cofixpoint_exprval sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexplib.Sexp.tval local_decl_expr_of_sexp : Sexplib.Sexp.t -> local_decl_exprval sexp_of_local_decl_expr : local_decl_expr -> Sexplib.Sexp.tval inductive_kind_of_sexp : Sexplib.Sexp.t -> inductive_kindval sexp_of_inductive_kind : inductive_kind -> Sexplib.Sexp.tval decl_notation_of_sexp : Sexplib.Sexp.t -> decl_notationval sexp_of_decl_notation : decl_notation -> Sexplib.Sexp.tval simple_binder_of_sexp : Sexplib.Sexp.t -> simple_binderval sexp_of_simple_binder : simple_binder -> Sexplib.Sexp.tval class_binder_of_sexp : Sexplib.Sexp.t -> class_binderval sexp_of_class_binder : class_binder -> Sexplib.Sexp.tval with_coercion_of_sexp :
(Sexplib.Sexp.t -> 'a) ->
Sexplib.Sexp.t ->
'a with_coercionval sexp_of_with_coercion :
('a -> Sexplib.Sexp.t) ->
'a with_coercion ->
Sexplib.Sexp.tval constructor_expr_of_sexp : Sexplib.Sexp.t -> constructor_exprval sexp_of_constructor_expr : constructor_expr -> Sexplib.Sexp.tval constructor_list_or_record_decl_expr_of_sexp :
Sexplib.Sexp.t ->
constructor_list_or_record_decl_exprval sexp_of_constructor_list_or_record_decl_expr :
constructor_list_or_record_decl_expr ->
Sexplib.Sexp.tval inductive_expr_of_sexp : Sexplib.Sexp.t -> inductive_exprval sexp_of_inductive_expr : inductive_expr -> Sexplib.Sexp.tval one_inductive_expr_of_sexp : Sexplib.Sexp.t -> one_inductive_exprval sexp_of_one_inductive_expr : one_inductive_expr -> Sexplib.Sexp.tval proof_expr_of_sexp : Sexplib.Sexp.t -> proof_exprval sexp_of_proof_expr : proof_expr -> Sexplib.Sexp.tval proof_end_of_sexp : Sexplib.Sexp.t -> proof_endval sexp_of_proof_end : proof_end -> Sexplib.Sexp.tval scheme_of_sexp : Sexplib.Sexp.t -> schemeval sexp_of_scheme : scheme -> Sexplib.Sexp.tval section_subset_expr_of_sexp : Sexplib.Sexp.t -> section_subset_exprval sexp_of_section_subset_expr : section_subset_expr -> Sexplib.Sexp.tval extend_name_of_sexp : Sexplib.Sexp.t -> extend_nameval sexp_of_extend_name : extend_name -> Sexplib.Sexp.tval register_kind_of_sexp : Sexplib.Sexp.t -> register_kindval sexp_of_register_kind : register_kind -> Sexplib.Sexp.tval module_ast_inl_of_sexp : Sexplib.Sexp.t -> module_ast_inlval sexp_of_module_ast_inl : module_ast_inl -> Sexplib.Sexp.tval module_binder_of_sexp : Sexplib.Sexp.t -> module_binderval sexp_of_module_binder : module_binder -> Sexplib.Sexp.tval vernac_expr_of_sexp : Sexplib.Sexp.t -> vernac_exprval sexp_of_vernac_expr : vernac_expr -> Sexplib.Sexp.tval vernac_expr_of_yojson :
Yojson.Safe.t ->
(vernac_expr, string) Result.resultval vernac_expr_to_yojson : vernac_expr -> Yojson.Safe.tval vernac_control_of_sexp : Sexplib.Sexp.t -> vernac_controlval sexp_of_vernac_control : vernac_control -> Sexplib.Sexp.tval vernac_control_of_yojson :
Yojson.Safe.t ->
(vernac_control, string) Result.resultval vernac_control_to_yojson : vernac_control -> Yojson.Safe.t