package coq-serapi

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

Install 

dune-project
 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.12.0.0.12.0.tbz
sha256=7a50234b5a78be69fcf2f51463fb993a31cc9c1fafc7ac6c7fe081cd0f18b43f
sha512=1f76b8fcc452db99a5a90be68cc58e083c3636259c0bada7b38c71698ae377a71bc115df0a8814a4dc831c953a998dcaf1e17e9e57bd48810bcd2eddbc6757fd

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

Module Serlib.Ser_constrexpr

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 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 abstraction_kind = Constrexpr.abstraction_kind
val abstraction_kind_of_sexp : Sexplib.Sexp.t -> abstraction_kind
val sexp_of_abstraction_kind : abstraction_kind -> Sexplib.Sexp.t
type proj_flag = Constrexpr.proj_flag
val proj_flag_of_sexp : Sexplib.Sexp.t -> proj_flag
val sexp_of_proj_flag : proj_flag -> 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