package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.10.0.0.7.1.tbz
sha256=207b091d8d9d9e1a649759f0acfd15cbfda54a2627a01fc74aa74ec0ffaa3400
sha512=af85d00c5896e78a6edea7794070795ca14c8e47a0e9a28f2ac003364b0f99eb72f19f57e755a3967d255b1aaf62cae0d09bbab02d2d35ef6ee02b84823a0929

doc/coq-serapi.serlib/Serlib/Ser_vernacexpr/index.html

Module Serlib.Ser_vernacexpr

type class_rawexpr = Vernacexpr.class_rawexpr
val class_rawexpr_of_sexp : Sexplib.Sexp.t -> class_rawexpr
val sexp_of_class_rawexpr : class_rawexpr -> Sexplib.Sexp.t
type goal_identifier = Vernacexpr.goal_identifier
val goal_identifier_of_sexp : Sexplib.Sexp.t -> goal_identifier
val sexp_of_goal_identifier : goal_identifier -> Sexplib.Sexp.t
type scope_name = Vernacexpr.scope_name
val scope_name_of_sexp : Sexplib.Sexp.t -> scope_name
val sexp_of_scope_name : scope_name -> Sexplib.Sexp.t
type goal_reference = Vernacexpr.goal_reference
val goal_reference_of_sexp : Sexplib.Sexp.t -> goal_reference
val sexp_of_goal_reference : goal_reference -> Sexplib.Sexp.t
type printable = Vernacexpr.printable
val printable_of_sexp : Sexplib.Sexp.t -> printable
val sexp_of_printable : printable -> Sexplib.Sexp.t
type search_about_item = Vernacexpr.search_about_item
val search_about_item_of_sexp : Sexplib.Sexp.t -> search_about_item
val sexp_of_search_about_item : search_about_item -> Sexplib.Sexp.t
type searchable = Vernacexpr.searchable
val searchable_of_sexp : Sexplib.Sexp.t -> searchable
val sexp_of_searchable : searchable -> Sexplib.Sexp.t
type locatable = Vernacexpr.locatable
val locatable_of_sexp : Sexplib.Sexp.t -> locatable
val sexp_of_locatable : locatable -> Sexplib.Sexp.t
type showable = Vernacexpr.showable
val showable_of_sexp : Sexplib.Sexp.t -> showable
val sexp_of_showable : showable -> Sexplib.Sexp.t
type comment = Vernacexpr.comment
val comment_of_sexp : Sexplib.Sexp.t -> comment
val sexp_of_comment : comment -> Sexplib.Sexp.t
type search_restriction = Vernacexpr.search_restriction
val search_restriction_of_sexp : Sexplib.Sexp.t -> search_restriction
val sexp_of_search_restriction : search_restriction -> Sexplib.Sexp.t
type rec_flag = Vernacexpr.rec_flag
val rec_flag_of_sexp : Sexplib.Sexp.t -> rec_flag
val sexp_of_rec_flag : rec_flag -> Sexplib.Sexp.t
type verbose_flag = Vernacexpr.verbose_flag
val verbose_flag_of_sexp : Sexplib.Sexp.t -> verbose_flag
val sexp_of_verbose_flag : verbose_flag -> Sexplib.Sexp.t
type coercion_flag = Vernacexpr.coercion_flag
val coercion_flag_of_sexp : Sexplib.Sexp.t -> coercion_flag
val sexp_of_coercion_flag : coercion_flag -> Sexplib.Sexp.t
type inductive_flag = Vernacexpr.inductive_flag
val inductive_flag_of_sexp : Sexplib.Sexp.t -> inductive_flag
val sexp_of_inductive_flag : inductive_flag -> Sexplib.Sexp.t
type instance_flag = Vernacexpr.instance_flag
val instance_flag_of_sexp : Sexplib.Sexp.t -> instance_flag
val sexp_of_instance_flag : instance_flag -> Sexplib.Sexp.t
type export_flag = Vernacexpr.export_flag
val export_flag_of_sexp : Sexplib.Sexp.t -> export_flag
val sexp_of_export_flag : export_flag -> Sexplib.Sexp.t
type onlyparsing_flag = Vernacexpr.onlyparsing_flag
val onlyparsing_flag_of_sexp : Sexplib.Sexp.t -> onlyparsing_flag
val sexp_of_onlyparsing_flag : onlyparsing_flag -> Sexplib.Sexp.t
type locality_flag = Vernacexpr.locality_flag
val locality_flag_of_sexp : Sexplib.Sexp.t -> locality_flag
val sexp_of_locality_flag : locality_flag -> Sexplib.Sexp.t
type option_ref_value = Vernacexpr.option_ref_value
val option_ref_value_of_sexp : Sexplib.Sexp.t -> option_ref_value
val sexp_of_option_ref_value : option_ref_value -> Sexplib.Sexp.t
type sort_expr = Vernacexpr.sort_expr
val sort_expr_of_sexp : Sexplib.Sexp.t -> sort_expr
val sexp_of_sort_expr : sort_expr -> Sexplib.Sexp.t
type definition_expr = Vernacexpr.definition_expr
val definition_expr_of_sexp : Sexplib.Sexp.t -> definition_expr
val sexp_of_definition_expr : definition_expr -> Sexplib.Sexp.t
type fixpoint_expr = Vernacexpr.fixpoint_expr
val fixpoint_expr_of_sexp : Sexplib.Sexp.t -> fixpoint_expr
val sexp_of_fixpoint_expr : fixpoint_expr -> Sexplib.Sexp.t
type cofixpoint_expr = Vernacexpr.cofixpoint_expr
val cofixpoint_expr_of_sexp : Sexplib.Sexp.t -> cofixpoint_expr
val sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexplib.Sexp.t
type local_decl_expr = Vernacexpr.local_decl_expr
val local_decl_expr_of_sexp : Sexplib.Sexp.t -> local_decl_expr
val sexp_of_local_decl_expr : local_decl_expr -> Sexplib.Sexp.t
type inductive_kind = Vernacexpr.inductive_kind
val inductive_kind_of_sexp : Sexplib.Sexp.t -> inductive_kind
val sexp_of_inductive_kind : inductive_kind -> Sexplib.Sexp.t
type decl_notation = Vernacexpr.decl_notation
val decl_notation_of_sexp : Sexplib.Sexp.t -> decl_notation
val sexp_of_decl_notation : decl_notation -> Sexplib.Sexp.t
type simple_binder = Vernacexpr.simple_binder
val simple_binder_of_sexp : Sexplib.Sexp.t -> simple_binder
val sexp_of_simple_binder : simple_binder -> Sexplib.Sexp.t
type class_binder = Vernacexpr.class_binder
val class_binder_of_sexp : Sexplib.Sexp.t -> class_binder
val sexp_of_class_binder : class_binder -> Sexplib.Sexp.t
type 'a with_coercion = 'a Vernacexpr.with_coercion
val with_coercion_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_coercion
val sexp_of_with_coercion : ('a -> Sexplib.Sexp.t) -> 'a with_coercion -> Sexplib.Sexp.t
type 'a with_instance = 'a Vernacexpr.with_instance
val with_instance_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_instance
val sexp_of_with_instance : ('a -> Sexplib.Sexp.t) -> 'a with_instance -> Sexplib.Sexp.t
type 'a with_notation = 'a Vernacexpr.with_notation
val with_notation_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_notation
val sexp_of_with_notation : ('a -> Sexplib.Sexp.t) -> 'a with_notation -> Sexplib.Sexp.t
type 'a with_priority = 'a Vernacexpr.with_priority
val with_priority_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_priority
val sexp_of_with_priority : ('a -> Sexplib.Sexp.t) -> 'a with_priority -> Sexplib.Sexp.t
type constructor_expr = Vernacexpr.constructor_expr
val constructor_expr_of_sexp : Sexplib.Sexp.t -> constructor_expr
val sexp_of_constructor_expr : constructor_expr -> Sexplib.Sexp.t
type constructor_list_or_record_decl_expr = Vernacexpr.constructor_list_or_record_decl_expr
val constructor_list_or_record_decl_expr_of_sexp : Sexplib.Sexp.t -> constructor_list_or_record_decl_expr
val sexp_of_constructor_list_or_record_decl_expr : constructor_list_or_record_decl_expr -> Sexplib.Sexp.t
type inductive_expr = Vernacexpr.inductive_expr
val inductive_expr_of_sexp : Sexplib.Sexp.t -> inductive_expr
val sexp_of_inductive_expr : inductive_expr -> Sexplib.Sexp.t
type one_inductive_expr = Vernacexpr.one_inductive_expr
val one_inductive_expr_of_sexp : Sexplib.Sexp.t -> one_inductive_expr
val sexp_of_one_inductive_expr : one_inductive_expr -> Sexplib.Sexp.t
type proof_expr = Vernacexpr.proof_expr
val proof_expr_of_sexp : Sexplib.Sexp.t -> proof_expr
val sexp_of_proof_expr : proof_expr -> Sexplib.Sexp.t
type proof_end = Vernacexpr.proof_end
val proof_end_of_sexp : Sexplib.Sexp.t -> proof_end
val sexp_of_proof_end : proof_end -> Sexplib.Sexp.t
type scheme = Vernacexpr.scheme
val scheme_of_sexp : Sexplib.Sexp.t -> scheme
val sexp_of_scheme : scheme -> Sexplib.Sexp.t
type section_subset_expr = Vernacexpr.section_subset_expr
val section_subset_expr_of_sexp : Sexplib.Sexp.t -> section_subset_expr
val sexp_of_section_subset_expr : section_subset_expr -> Sexplib.Sexp.t
type extend_name = Vernacexpr.extend_name
val extend_name_of_sexp : Sexplib.Sexp.t -> extend_name
val sexp_of_extend_name : extend_name -> Sexplib.Sexp.t
type register_kind = Vernacexpr.register_kind
val register_kind_of_sexp : Sexplib.Sexp.t -> register_kind
val sexp_of_register_kind : register_kind -> Sexplib.Sexp.t
type module_ast_inl = Vernacexpr.module_ast_inl
val module_ast_inl_of_sexp : Sexplib.Sexp.t -> module_ast_inl
val sexp_of_module_ast_inl : module_ast_inl -> Sexplib.Sexp.t
type module_binder = Vernacexpr.module_binder
val module_binder_of_sexp : Sexplib.Sexp.t -> module_binder
val sexp_of_module_binder : module_binder -> Sexplib.Sexp.t
type vernac_expr = Vernacexpr.vernac_expr
val vernac_expr_of_sexp : Sexplib.Sexp.t -> vernac_expr
val sexp_of_vernac_expr : vernac_expr -> Sexplib.Sexp.t
val vernac_expr_of_yojson : Yojson.Safe.t -> (vernac_expr, string) Result.result
val vernac_expr_to_yojson : vernac_expr -> Yojson.Safe.t
type vernac_control = Vernacexpr.vernac_control
val vernac_control_of_sexp : Sexplib.Sexp.t -> vernac_control
val sexp_of_vernac_control : vernac_control -> Sexplib.Sexp.t
val vernac_control_of_yojson : Yojson.Safe.t -> (vernac_control, string) Result.result
val vernac_control_to_yojson : vernac_control -> Yojson.Safe.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct