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.19.0.0.19.0.tbz
sha256=28792fdef7dbcc8a21a3eee1a85d6c433eccde6a85c47d73c8f808c02aa232fd
sha512=b5f8142df58f10639e2aa77209496e5906f5ce69f7bd93a65c9519d539a5546015e4760e0e980c277ab2d908c8cc77eb0d46ae7c1a9ca1fbca985b4c825b891f

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

Module Serlib.Ser_constrexprSource

Sourcetype 'a or_by_notation = 'a Constrexpr.or_by_notation
Sourceval sexp_of_or_by_notation : ('a -> Sexplib0.Sexp.t) -> 'a or_by_notation -> Sexplib0.Sexp.t
Sourceval or_by_notation_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a or_by_notation
Sourceval or_by_notation_to_yojson : ('a -> Yojson.Safe.t) -> 'a or_by_notation -> Yojson.Safe.t
Sourceval hash_fold_or_by_notation : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a or_by_notation -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_or_by_notation : ('a -> 'a -> int) -> 'a or_by_notation -> 'a or_by_notation -> int
Sourcetype notation_entry = Constrexpr.notation_entry
Sourceval sexp_of_notation_entry : notation_entry -> Sexplib0.Sexp.t
Sourceval notation_entry_of_sexp : Sexplib0.Sexp.t -> notation_entry
Sourceval notation_entry_to_yojson : notation_entry -> Yojson.Safe.t
Sourceval notation_entry_of_yojson : Yojson.Safe.t -> notation_entry Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_notation_entry : Ppx_hash_lib.Std.Hash.state -> notation_entry -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_notation_entry : notation_entry -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_notation_entry : notation_entry -> notation_entry -> int
Sourcetype entry_level = Constrexpr.entry_level
Sourceval sexp_of_entry_level : entry_level -> Sexplib0.Sexp.t
Sourceval entry_level_of_sexp : Sexplib0.Sexp.t -> entry_level
Sourceval entry_level_to_yojson : entry_level -> Yojson.Safe.t
Sourceval entry_level_of_yojson : Yojson.Safe.t -> entry_level Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_entry_level : Ppx_hash_lib.Std.Hash.state -> entry_level -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_entry_level : entry_level -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_entry_level : entry_level -> entry_level -> int
Sourcetype notation_entry_level = Constrexpr.notation_entry_level
Sourceval sexp_of_notation_entry_level : notation_entry_level -> Sexplib0.Sexp.t
Sourceval notation_entry_level_of_sexp : Sexplib0.Sexp.t -> notation_entry_level
Sourceval notation_entry_level_to_yojson : notation_entry_level -> Yojson.Safe.t
Sourceval notation_entry_level_of_yojson : Yojson.Safe.t -> notation_entry_level Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_notation_entry_level : Ppx_hash_lib.Std.Hash.state -> notation_entry_level -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_notation_entry_level : notation_entry_level -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_notation_entry_level : notation_entry_level -> notation_entry_level -> int
Sourcetype entry_relative_level = Constrexpr.entry_relative_level
Sourceval sexp_of_entry_relative_level : entry_relative_level -> Sexplib0.Sexp.t
Sourceval entry_relative_level_of_sexp : Sexplib0.Sexp.t -> entry_relative_level
Sourceval entry_relative_level_to_yojson : entry_relative_level -> Yojson.Safe.t
Sourceval entry_relative_level_of_yojson : Yojson.Safe.t -> entry_relative_level Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_entry_relative_level : Ppx_hash_lib.Std.Hash.state -> entry_relative_level -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_entry_relative_level : entry_relative_level -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_entry_relative_level : entry_relative_level -> entry_relative_level -> int
Sourcetype notation_entry_relative_level = Constrexpr.notation_entry_relative_level
Sourceval sexp_of_notation_entry_relative_level : notation_entry_relative_level -> Sexplib0.Sexp.t
Sourceval notation_entry_relative_level_of_sexp : Sexplib0.Sexp.t -> notation_entry_relative_level
Sourceval notation_entry_relative_level_to_yojson : notation_entry_relative_level -> Yojson.Safe.t
Sourceval notation_entry_relative_level_of_yojson : Yojson.Safe.t -> notation_entry_relative_level Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_notation_entry_relative_level : Ppx_hash_lib.Std.Hash.state -> notation_entry_relative_level -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_notation_entry_relative_level : notation_entry_relative_level -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_notation_entry_relative_level : notation_entry_relative_level -> notation_entry_relative_level -> int
Sourcetype universe_decl_expr = Constrexpr.universe_decl_expr
Sourceval sexp_of_universe_decl_expr : universe_decl_expr -> Sexplib0.Sexp.t
Sourceval universe_decl_expr_of_sexp : Sexplib0.Sexp.t -> universe_decl_expr
Sourceval universe_decl_expr_to_yojson : universe_decl_expr -> Yojson.Safe.t
Sourceval hash_fold_universe_decl_expr : Ppx_hash_lib.Std.Hash.state -> universe_decl_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_universe_decl_expr : universe_decl_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_universe_decl_expr : universe_decl_expr -> universe_decl_expr -> int
Sourcetype ident_decl = Constrexpr.ident_decl
Sourceval sexp_of_ident_decl : ident_decl -> Sexplib0.Sexp.t
Sourceval ident_decl_of_sexp : Sexplib0.Sexp.t -> ident_decl
Sourceval ident_decl_to_yojson : ident_decl -> Yojson.Safe.t
Sourceval hash_fold_ident_decl : Ppx_hash_lib.Std.Hash.state -> ident_decl -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ident_decl : ident_decl -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ident_decl : ident_decl -> ident_decl -> int
Sourcetype cumul_ident_decl = Constrexpr.cumul_ident_decl
Sourceval sexp_of_cumul_ident_decl : cumul_ident_decl -> Sexplib0.Sexp.t
Sourceval cumul_ident_decl_of_sexp : Sexplib0.Sexp.t -> cumul_ident_decl
Sourceval cumul_ident_decl_to_yojson : cumul_ident_decl -> Yojson.Safe.t
Sourceval hash_fold_cumul_ident_decl : Ppx_hash_lib.Std.Hash.state -> cumul_ident_decl -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_cumul_ident_decl : cumul_ident_decl -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_cumul_ident_decl : cumul_ident_decl -> cumul_ident_decl -> int
Sourcetype univ_constraint_expr = Constrexpr.univ_constraint_expr
Sourceval sexp_of_univ_constraint_expr : univ_constraint_expr -> Sexplib0.Sexp.t
Sourceval univ_constraint_expr_of_sexp : Sexplib0.Sexp.t -> univ_constraint_expr
Sourceval univ_constraint_expr_to_yojson : univ_constraint_expr -> Yojson.Safe.t
Sourceval hash_fold_univ_constraint_expr : Ppx_hash_lib.Std.Hash.state -> univ_constraint_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_univ_constraint_expr : univ_constraint_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_univ_constraint_expr : univ_constraint_expr -> univ_constraint_expr -> int
Sourcetype name_decl = Constrexpr.name_decl
Sourceval sexp_of_name_decl : name_decl -> Sexplib0.Sexp.t
Sourceval name_decl_of_sexp : Sexplib0.Sexp.t -> name_decl
Sourceval name_decl_to_yojson : name_decl -> Yojson.Safe.t
Sourceval hash_fold_name_decl : Ppx_hash_lib.Std.Hash.state -> name_decl -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_name_decl : name_decl -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_name_decl : name_decl -> name_decl -> int
Sourcetype notation_with_optional_scope = Constrexpr.notation_with_optional_scope
Sourceval sexp_of_notation_with_optional_scope : notation_with_optional_scope -> Sexplib0.Sexp.t
Sourceval notation_with_optional_scope_of_sexp : Sexplib0.Sexp.t -> notation_with_optional_scope
Sourceval notation_with_optional_scope_to_yojson : notation_with_optional_scope -> Yojson.Safe.t
Sourceval hash_fold_notation_with_optional_scope : Ppx_hash_lib.Std.Hash.state -> notation_with_optional_scope -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_notation_with_optional_scope : notation_with_optional_scope -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_notation_with_optional_scope : notation_with_optional_scope -> notation_with_optional_scope -> int
Sourcetype side = Constrexpr.side
Sourceval sexp_of_side : side -> Sexplib0.Sexp.t
Sourceval side_of_sexp : Sexplib0.Sexp.t -> side
Sourceval side_to_yojson : side -> Yojson.Safe.t
Sourceval hash_fold_side : Ppx_hash_lib.Std.Hash.state -> side -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_side : side -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_side : side -> side -> int
Sourcetype notation = Constrexpr.notation
Sourceval notation_of_sexp : Sexplib.Sexp.t -> notation
Sourceval sexp_of_notation : notation -> Sexplib.Sexp.t
Sourcetype explicitation = Constrexpr.explicitation
Sourceval explicitation_of_sexp : Sexplib.Sexp.t -> explicitation
Sourceval sexp_of_explicitation : explicitation -> Sexplib.Sexp.t
Sourcetype binder_kind = Constrexpr.binder_kind
Sourceval binder_kind_of_sexp : Sexplib.Sexp.t -> binder_kind
Sourceval sexp_of_binder_kind : binder_kind -> Sexplib.Sexp.t
Sourcetype delimiter_depth = Constrexpr.delimiter_depth =
  1. | DelimOnlyTmpScope
  2. | DelimUnboundedScope
Sourceval sexp_of_delimiter_depth : delimiter_depth -> Sexplib0.Sexp.t
Sourceval delimiter_depth_of_sexp : Sexplib0.Sexp.t -> delimiter_depth
Sourceval delimiter_depth_to_yojson : delimiter_depth -> Yojson.Safe.t
Sourceval hash_fold_delimiter_depth : Ppx_hash_lib.Std.Hash.state -> delimiter_depth -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_delimiter_depth : delimiter_depth -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_delimiter_depth : delimiter_depth -> delimiter_depth -> int
Sourcetype prim_token = Constrexpr.prim_token
Sourceval prim_token_of_sexp : Sexplib.Sexp.t -> prim_token
Sourceval sexp_of_prim_token : prim_token -> Sexplib.Sexp.t
Sourcetype cases_pattern_expr = Constrexpr.cases_pattern_expr
Sourceand cases_pattern_notation_substitution = Constrexpr.cases_pattern_notation_substitution
Sourceval cases_pattern_expr_of_sexp : Sexplib.Sexp.t -> cases_pattern_expr
Sourceval cases_pattern_notation_substitution_of_sexp : Sexplib.Sexp.t -> cases_pattern_notation_substitution
Sourceval sexp_of_cases_pattern_expr : cases_pattern_expr -> Sexplib.Sexp.t
Sourceval sexp_of_cases_pattern_notation_substitution : cases_pattern_notation_substitution -> Sexplib.Sexp.t
Sourcetype instance_expr = Constrexpr.instance_expr
Sourceval instance_expr_of_sexp : Sexplib.Sexp.t -> instance_expr
Sourceval sexp_of_instance_expr : instance_expr -> Sexplib.Sexp.t
Sourcetype constr_expr = Constrexpr.constr_expr
Sourceand case_expr = Constrexpr.case_expr
Sourceand branch_expr = Constrexpr.branch_expr
Sourceand fix_expr = Constrexpr.fix_expr
Sourceand cofix_expr = Constrexpr.cofix_expr
Sourceand recursion_order_expr = Constrexpr.recursion_order_expr
Sourceand local_binder_expr = Constrexpr.local_binder_expr
Sourceand constr_notation_substitution = Constrexpr.constr_notation_substitution
Sourceval sexp_of_constr_expr : constr_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_case_expr : case_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_branch_expr : branch_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_fix_expr : fix_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_cofix_expr : cofix_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_recursion_order_expr : recursion_order_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_local_binder_expr : local_binder_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_constr_notation_substitution : constr_notation_substitution -> Sexplib0.Sexp.t
Sourceval constr_expr_of_sexp : Sexplib0.Sexp.t -> constr_expr
Sourceval case_expr_of_sexp : Sexplib0.Sexp.t -> case_expr
Sourceval branch_expr_of_sexp : Sexplib0.Sexp.t -> branch_expr
Sourceval fix_expr_of_sexp : Sexplib0.Sexp.t -> fix_expr
Sourceval cofix_expr_of_sexp : Sexplib0.Sexp.t -> cofix_expr
Sourceval recursion_order_expr_of_sexp : Sexplib0.Sexp.t -> recursion_order_expr
Sourceval local_binder_expr_of_sexp : Sexplib0.Sexp.t -> local_binder_expr
Sourceval constr_notation_substitution_of_sexp : Sexplib0.Sexp.t -> constr_notation_substitution
Sourceval constr_expr_to_yojson : constr_expr -> Yojson.Safe.t
Sourceval case_expr_to_yojson : case_expr -> Yojson.Safe.t
Sourceval branch_expr_to_yojson : branch_expr -> Yojson.Safe.t
Sourceval fix_expr_to_yojson : fix_expr -> Yojson.Safe.t
Sourceval cofix_expr_to_yojson : cofix_expr -> Yojson.Safe.t
Sourceval recursion_order_expr_to_yojson : recursion_order_expr -> Yojson.Safe.t
Sourceval local_binder_expr_to_yojson : local_binder_expr -> Yojson.Safe.t
Sourceval constr_notation_substitution_to_yojson : constr_notation_substitution -> Yojson.Safe.t
Sourceval hash_fold_constr_expr : Ppx_hash_lib.Std.Hash.state -> constr_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_constr_expr : constr_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_fold_case_expr : Ppx_hash_lib.Std.Hash.state -> case_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_case_expr : case_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_fold_branch_expr : Ppx_hash_lib.Std.Hash.state -> branch_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_branch_expr : branch_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_fold_fix_expr : Ppx_hash_lib.Std.Hash.state -> fix_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_fix_expr : fix_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_fold_cofix_expr : Ppx_hash_lib.Std.Hash.state -> cofix_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_cofix_expr : cofix_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_fold_recursion_order_expr : Ppx_hash_lib.Std.Hash.state -> recursion_order_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_recursion_order_expr : recursion_order_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_fold_local_binder_expr : Ppx_hash_lib.Std.Hash.state -> local_binder_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_local_binder_expr : local_binder_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_fold_constr_notation_substitution : Ppx_hash_lib.Std.Hash.state -> constr_notation_substitution -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_constr_notation_substitution : constr_notation_substitution -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_constr_expr : constr_expr -> constr_expr -> int
Sourceval compare_case_expr : case_expr -> case_expr -> int
Sourceval compare_branch_expr : branch_expr -> branch_expr -> int
Sourceval compare_fix_expr : fix_expr -> fix_expr -> int
Sourceval compare_cofix_expr : cofix_expr -> cofix_expr -> int
Sourceval compare_recursion_order_expr : recursion_order_expr -> recursion_order_expr -> int
Sourceval compare_local_binder_expr : local_binder_expr -> local_binder_expr -> int
Sourceval compare_constr_notation_substitution : constr_notation_substitution -> constr_notation_substitution -> int
Sourcetype constr_pattern_expr = Constrexpr.constr_pattern_expr
Sourceval sexp_of_constr_pattern_expr : constr_pattern_expr -> Sexplib0.Sexp.t
Sourceval constr_pattern_expr_of_sexp : Sexplib0.Sexp.t -> constr_pattern_expr
Sourceval constr_pattern_expr_to_yojson : constr_pattern_expr -> Yojson.Safe.t
Sourceval hash_fold_constr_pattern_expr : Ppx_hash_lib.Std.Hash.state -> constr_pattern_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_constr_pattern_expr : constr_pattern_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_constr_pattern_expr : constr_pattern_expr -> constr_pattern_expr -> int
Sourcetype with_declaration_ast = Constrexpr.with_declaration_ast
Sourceval with_declaration_ast_of_sexp : Sexplib.Sexp.t -> with_declaration_ast
Sourceval sexp_of_with_declaration_ast : with_declaration_ast -> Sexplib.Sexp.t
Sourceval with_declaration_ast_of_yojson : Yojson.Safe.t -> (with_declaration_ast, string) Result.result
Sourceval with_declaration_ast_to_yojson : with_declaration_ast -> Yojson.Safe.t
Sourcetype module_ast = Constrexpr.module_ast
Sourceval sexp_of_module_ast : module_ast -> Sexplib0.Sexp.t
Sourceval module_ast_of_sexp : Sexplib0.Sexp.t -> module_ast
Sourceval module_ast_to_yojson : module_ast -> Yojson.Safe.t
Sourceval hash_fold_module_ast : Ppx_hash_lib.Std.Hash.state -> module_ast -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_module_ast : module_ast -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_module_ast : module_ast -> module_ast -> int
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