Module `Serlib.Ser_constrexpr`Source

Sourcetype '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

Source

val or_by_notation_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a or_by_notation

Source

val or_by_notation_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a or_by_notation ->
  Yojson.Safe.t

Source

val or_by_notation_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a or_by_notation Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val 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

Source

val notation_entry_of_yojson : 
  Yojson.Safe.t ->
  notation_entry Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val entry_level_of_yojson : 
  Yojson.Safe.t ->
  entry_level Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val notation_entry_level_of_yojson : 
  Yojson.Safe.t ->
  notation_entry_level Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_notation_entry_level : 
  Ppx_hash_lib.Std.Hash.state ->
  notation_entry_level ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_notation_entry_level : 
  notation_entry_level ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val 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

Source

val entry_relative_level_of_yojson : 
  Yojson.Safe.t ->
  entry_relative_level Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_entry_relative_level : 
  Ppx_hash_lib.Std.Hash.state ->
  entry_relative_level ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_entry_relative_level : 
  entry_relative_level ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_entry_relative_level : 
  entry_relative_level ->
  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

Source

val universe_decl_expr_of_yojson : 
  Yojson.Safe.t ->
  universe_decl_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_universe_decl_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  universe_decl_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_universe_decl_expr : 
  universe_decl_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val 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

Source

val ident_decl_of_yojson : 
  Yojson.Safe.t ->
  ident_decl Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val cumul_ident_decl_of_yojson : 
  Yojson.Safe.t ->
  cumul_ident_decl Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_cumul_ident_decl : 
  Ppx_hash_lib.Std.Hash.state ->
  cumul_ident_decl ->
  Ppx_hash_lib.Std.Hash.state

Source

val 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

Source

val univ_constraint_expr_of_yojson : 
  Yojson.Safe.t ->
  univ_constraint_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_univ_constraint_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  univ_constraint_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_univ_constraint_expr : 
  univ_constraint_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val 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

Source

val name_decl_of_yojson : 
  Yojson.Safe.t ->
  name_decl Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val sexp_of_notation_with_optional_scope : 
  notation_with_optional_scope ->
  Sexplib0.Sexp.t

Source

val notation_with_optional_scope_of_sexp : 
  Sexplib0.Sexp.t ->
  notation_with_optional_scope

Source

val notation_with_optional_scope_to_yojson : 
  notation_with_optional_scope ->
  Yojson.Safe.t

Source

val notation_with_optional_scope_of_yojson : 
  Yojson.Safe.t ->
  notation_with_optional_scope Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_notation_with_optional_scope : 
  Ppx_hash_lib.Std.Hash.state ->
  notation_with_optional_scope ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_notation_with_optional_scope : 
  notation_with_optional_scope ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_notation_with_optional_scope : 
  notation_with_optional_scope ->
  notation_with_optional_scope ->
  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 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

Source

and cases_pattern_notation_substitution =
  Constrexpr.cases_pattern_notation_substitution

Sourceval cases_pattern_expr_of_sexp : Sexplib.Sexp.t -> cases_pattern_expr

Source

val 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

Source

val 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

Source

val 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

Source

val constr_notation_substitution_of_sexp : 
  Sexplib0.Sexp.t ->
  constr_notation_substitution

Sourceval constr_expr_to_yojson : constr_expr -> Yojson.Safe.t

Source

val constr_expr_of_yojson : 
  Yojson.Safe.t ->
  constr_expr Ppx_deriving_yojson_runtime.error_or

Sourceval case_expr_to_yojson : case_expr -> Yojson.Safe.t

Source

val case_expr_of_yojson : 
  Yojson.Safe.t ->
  case_expr Ppx_deriving_yojson_runtime.error_or

Sourceval branch_expr_to_yojson : branch_expr -> Yojson.Safe.t

Source

val branch_expr_of_yojson : 
  Yojson.Safe.t ->
  branch_expr Ppx_deriving_yojson_runtime.error_or

Sourceval fix_expr_to_yojson : fix_expr -> Yojson.Safe.t

Source

val fix_expr_of_yojson : 
  Yojson.Safe.t ->
  fix_expr Ppx_deriving_yojson_runtime.error_or

Sourceval cofix_expr_to_yojson : cofix_expr -> Yojson.Safe.t

Source

val cofix_expr_of_yojson : 
  Yojson.Safe.t ->
  cofix_expr Ppx_deriving_yojson_runtime.error_or

Sourceval recursion_order_expr_to_yojson : recursion_order_expr -> Yojson.Safe.t

Source

val recursion_order_expr_of_yojson : 
  Yojson.Safe.t ->
  recursion_order_expr Ppx_deriving_yojson_runtime.error_or

Sourceval local_binder_expr_to_yojson : local_binder_expr -> Yojson.Safe.t

Source

val local_binder_expr_of_yojson : 
  Yojson.Safe.t ->
  local_binder_expr Ppx_deriving_yojson_runtime.error_or

Source

val constr_notation_substitution_to_yojson : 
  constr_notation_substitution ->
  Yojson.Safe.t

Source

val constr_notation_substitution_of_yojson : 
  Yojson.Safe.t ->
  constr_notation_substitution Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val 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

Source

val 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

Source

val 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

Source

val 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

Source

val hash_fold_recursion_order_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  recursion_order_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_recursion_order_expr : 
  recursion_order_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val hash_fold_local_binder_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  local_binder_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_local_binder_expr : 
  local_binder_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val hash_fold_constr_notation_substitution : 
  Ppx_hash_lib.Std.Hash.state ->
  constr_notation_substitution ->
  Ppx_hash_lib.Std.Hash.state

Source

val 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

Source

val compare_recursion_order_expr : 
  recursion_order_expr ->
  recursion_order_expr ->
  int

Sourceval compare_local_binder_expr : local_binder_expr -> local_binder_expr -> int

Source

val 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

Source

val constr_pattern_expr_of_yojson : 
  Yojson.Safe.t ->
  constr_pattern_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_constr_pattern_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  constr_pattern_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_constr_pattern_expr : 
  constr_pattern_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val 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

Source

val 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

Source

val module_ast_of_yojson : 
  Yojson.Safe.t ->
  module_ast Ppx_deriving_yojson_runtime.error_or

Source

val 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

package coq-serapi

Module Serlib.Ser_constrexprSource

Module `Serlib.Ser_constrexpr`Source