package coq-serapi

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