coq-serapi 8.15.0+0.15.0 · OCaml Package

type 'a or_by_notation = 'a Constrexpr.or_by_notation

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

val sexp_of_or_by_notation : 
  ('a -> Sexplib.Sexp.t) ->
  'a or_by_notation ->
  Sexplib.Sexp.t

val or_by_notation_of_yojson : 
  (Yojson.Safe.t -> ('a, string) Result.result) ->
  Yojson.Safe.t ->
  ('a or_by_notation, string) Result.result

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

type notation_entry = Constrexpr.notation_entry

val notation_entry_of_sexp : Sexplib.Sexp.t -> notation_entry

val sexp_of_notation_entry : notation_entry -> Sexplib.Sexp.t

val notation_entry_of_yojson : 
  Yojson.Safe.t ->
  (notation_entry, string) Result.result

val notation_entry_to_yojson : notation_entry -> Yojson.Safe.t

type entry_level = Constrexpr.entry_level

val entry_level_of_sexp : Sexplib.Sexp.t -> entry_level

val sexp_of_entry_level : entry_level -> Sexplib.Sexp.t

val entry_level_of_yojson : 
  Yojson.Safe.t ->
  (entry_level, string) Result.result

val entry_level_to_yojson : entry_level -> Yojson.Safe.t

type notation_entry_level = Constrexpr.notation_entry_level

val notation_entry_level_of_sexp : Sexplib.Sexp.t -> notation_entry_level

val sexp_of_notation_entry_level : notation_entry_level -> Sexplib.Sexp.t

val notation_entry_level_of_yojson : 
  Yojson.Safe.t ->
  (notation_entry_level, string) Result.result

val notation_entry_level_to_yojson : notation_entry_level -> Yojson.Safe.t

type entry_relative_level = Constrexpr.entry_relative_level

val entry_relative_level_of_sexp : Sexplib.Sexp.t -> entry_relative_level

val sexp_of_entry_relative_level : entry_relative_level -> Sexplib.Sexp.t

val entry_relative_level_of_yojson : 
  Yojson.Safe.t ->
  (entry_relative_level, string) Result.result

val entry_relative_level_to_yojson : entry_relative_level -> Yojson.Safe.t

type universe_decl_expr = Constrexpr.universe_decl_expr

val universe_decl_expr_of_sexp : Sexplib.Sexp.t -> universe_decl_expr

val sexp_of_universe_decl_expr : universe_decl_expr -> Sexplib.Sexp.t

val universe_decl_expr_of_yojson : 
  Yojson.Safe.t ->
  (universe_decl_expr, string) Result.result

val universe_decl_expr_to_yojson : universe_decl_expr -> Yojson.Safe.t

type ident_decl = Constrexpr.ident_decl

val ident_decl_of_sexp : Sexplib.Sexp.t -> ident_decl

val sexp_of_ident_decl : ident_decl -> Sexplib.Sexp.t

val ident_decl_of_yojson : Yojson.Safe.t -> (ident_decl, string) Result.result

val ident_decl_to_yojson : ident_decl -> Yojson.Safe.t

type cumul_ident_decl = Constrexpr.cumul_ident_decl

val cumul_ident_decl_of_sexp : Sexplib.Sexp.t -> cumul_ident_decl

val sexp_of_cumul_ident_decl : cumul_ident_decl -> Sexplib.Sexp.t

val cumul_ident_decl_of_yojson : 
  Yojson.Safe.t ->
  (cumul_ident_decl, string) Result.result

val cumul_ident_decl_to_yojson : cumul_ident_decl -> Yojson.Safe.t

type univ_constraint_expr = Constrexpr.univ_constraint_expr

val univ_constraint_expr_of_sexp : Sexplib.Sexp.t -> univ_constraint_expr

val sexp_of_univ_constraint_expr : univ_constraint_expr -> Sexplib.Sexp.t

val univ_constraint_expr_of_yojson : 
  Yojson.Safe.t ->
  (univ_constraint_expr, string) Result.result

val univ_constraint_expr_to_yojson : univ_constraint_expr -> Yojson.Safe.t

type name_decl = Constrexpr.name_decl

val name_decl_of_sexp : Sexplib.Sexp.t -> name_decl

val sexp_of_name_decl : name_decl -> Sexplib.Sexp.t

val name_decl_of_yojson : Yojson.Safe.t -> (name_decl, string) Result.result

val name_decl_to_yojson : name_decl -> Yojson.Safe.t

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 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 constr_expr_of_sexp : Sexplib.Sexp.t -> constr_expr

val case_expr_of_sexp : Sexplib.Sexp.t -> case_expr

val branch_expr_of_sexp : Sexplib.Sexp.t -> branch_expr

val fix_expr_of_sexp : Sexplib.Sexp.t -> fix_expr

val cofix_expr_of_sexp : Sexplib.Sexp.t -> cofix_expr

val constr_notation_substitution_of_sexp : 
  Sexplib.Sexp.t ->
  constr_notation_substitution

val sexp_of_constr_expr : constr_expr -> Sexplib.Sexp.t

val sexp_of_case_expr : case_expr -> Sexplib.Sexp.t

val sexp_of_branch_expr : branch_expr -> Sexplib.Sexp.t

val sexp_of_fix_expr : fix_expr -> Sexplib.Sexp.t

val sexp_of_cofix_expr : cofix_expr -> Sexplib.Sexp.t

val sexp_of_constr_notation_substitution : 
  constr_notation_substitution ->
  Sexplib.Sexp.t

val recursion_order_expr_of_sexp : Sexplib.Sexp.t -> recursion_order_expr

val sexp_of_recursion_order_expr : recursion_order_expr -> Sexplib.Sexp.t

val recursion_order_expr_of_yojson : 
  Yojson.Safe.t ->
  (recursion_order_expr, string) Result.result

val recursion_order_expr_to_yojson : recursion_order_expr -> Yojson.Safe.t

val sexp_of_local_binder_expr : local_binder_expr -> Sexplib.Sexp.t

val local_binder_expr_of_sexp : Sexplib.Sexp.t -> local_binder_expr

val local_binder_expr_of_yojson : 
  Yojson.Safe.t ->
  (local_binder_expr, string) Result.result

val local_binder_expr_to_yojson : local_binder_expr -> Yojson.Safe.t

val constr_expr_of_yojson : 
  Yojson.Safe.t ->
  (constr_expr, string) Result.result

val constr_expr_to_yojson : constr_expr -> Yojson.Safe.t

type constr_pattern_expr = Constrexpr.constr_pattern_expr

val constr_pattern_expr_of_sexp : Sexplib.Sexp.t -> constr_pattern_expr

val sexp_of_constr_pattern_expr : constr_pattern_expr -> Sexplib.Sexp.t

val constr_pattern_expr_of_yojson : 
  Yojson.Safe.t ->
  (constr_pattern_expr, string) Result.result

val constr_pattern_expr_to_yojson : constr_pattern_expr -> Yojson.Safe.t

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 module_ast_of_sexp : Sexplib.Sexp.t -> module_ast

val sexp_of_module_ast : module_ast -> Sexplib.Sexp.t

val module_ast_of_yojson : Yojson.Safe.t -> (module_ast, string) Result.result

val module_ast_to_yojson : module_ast -> Yojson.Safe.t

package coq-serapi