package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Stateid = Ser_stateid
module Future = Ser_future
module Names = Ser_names
module Univ = Ser_univ
module UVars = Ser_uvars
module Constr = Ser_constr
module Declarations = Ser_declarations
module CPrimitives = Ser_cPrimitives
type universes_entry = Entries.universes_entry =
  1. | Monomorphic_entry
  2. | Polymorphic_entry of UVars.UContext.t
val universes_entry_of_sexp : Sexplib0.Sexp.t -> universes_entry
val sexp_of_universes_entry : universes_entry -> Sexplib0.Sexp.t
type 'a in_universes_entry = 'a * universes_entry
val in_universes_entry_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a in_universes_entry
val sexp_of_in_universes_entry : 'a. ('a -> Sexplib0.Sexp.t) -> 'a in_universes_entry -> Sexplib0.Sexp.t
type one_inductive_entry = Entries.one_inductive_entry = {
  1. mind_entry_typename : Names.Id.t;
  2. mind_entry_arity : Constr.constr;
  3. mind_entry_consnames : Names.Id.t list;
  4. mind_entry_lc : Constr.constr list;
}
val one_inductive_entry_of_sexp : Sexplib0.Sexp.t -> one_inductive_entry
val sexp_of_one_inductive_entry : one_inductive_entry -> Sexplib0.Sexp.t
type variance_entry = UVars.Variance.t option array
val variance_entry_of_sexp : Sexplib0.Sexp.t -> variance_entry
val sexp_of_variance_entry : variance_entry -> Sexplib0.Sexp.t
type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
val proof_output_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a proof_output
val sexp_of_proof_output : 'a. ('a -> Sexplib0.Sexp.t) -> 'a proof_output -> Sexplib0.Sexp.t
type definition_entry = Entries.definition_entry = {
  1. const_entry_body : Constr.constr;
  2. const_entry_secctx : Names.Id.Set.t option;
  3. const_entry_type : Constr.types option;
  4. const_entry_universes : universes_entry;
  5. const_entry_inline_code : bool;
}
val definition_entry_of_sexp : Sexplib0.Sexp.t -> definition_entry
val sexp_of_definition_entry : definition_entry -> Sexplib0.Sexp.t
type section_def_entry = Entries.section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_type : Constr.types option;
}
val section_def_entry_of_sexp : Sexplib0.Sexp.t -> section_def_entry
val sexp_of_section_def_entry : section_def_entry -> Sexplib0.Sexp.t
type inline = int option
val inline_of_sexp : Sexplib0.Sexp.t -> inline
val sexp_of_inline : inline -> Sexplib0.Sexp.t
type 'a opaque_entry = 'a Entries.opaque_entry = {
  1. opaque_entry_body : 'a;
  2. opaque_entry_secctx : Names.Id.Set.t;
  3. opaque_entry_type : Constr.types;
  4. opaque_entry_universes : universes_entry;
}
val opaque_entry_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a opaque_entry
val sexp_of_opaque_entry : 'a. ('a -> Sexplib0.Sexp.t) -> 'a opaque_entry -> Sexplib0.Sexp.t
type parameter_entry = Entries.parameter_entry = {
  1. parameter_entry_secctx : Names.Id.Set.t option;
  2. parameter_entry_type : Constr.types;
  3. parameter_entry_universes : universes_entry;
  4. parameter_entry_inline_code : inline;
}
val parameter_entry_of_sexp : Sexplib0.Sexp.t -> parameter_entry
val sexp_of_parameter_entry : parameter_entry -> Sexplib0.Sexp.t
type primitive_entry = Entries.primitive_entry = {
  1. prim_entry_type : Constr.types in_universes_entry option;
  2. prim_entry_content : CPrimitives.op_or_type;
}
val primitive_entry_of_sexp : Sexplib0.Sexp.t -> primitive_entry
val sexp_of_primitive_entry : primitive_entry -> Sexplib0.Sexp.t
type symbol_entry = Entries.symbol_entry = {
  1. symb_entry_type : Constr.types;
  2. symb_entry_unfold_fix : bool;
  3. symb_entry_universes : universes_entry;
}
val symbol_entry_of_sexp : Sexplib0.Sexp.t -> symbol_entry
val sexp_of_symbol_entry : symbol_entry -> Sexplib0.Sexp.t
type constant_entry = Entries.constant_entry =
  1. | DefinitionEntry : definition_entry -> constant_entry
  2. | ParameterEntry : parameter_entry -> constant_entry
  3. | PrimitiveEntry : primitive_entry -> constant_entry
  4. | SymbolEntry : symbol_entry -> constant_entry
val constant_entry_of_sexp : Sexplib0.Sexp.t -> constant_entry
val sexp_of_constant_entry : constant_entry -> Sexplib0.Sexp.t
type module_struct_entry = (Constr.constr * UVars.AbstractContext.t option) Declarations.module_alg_expr
val module_struct_entry_of_sexp : Sexplib0.Sexp.t -> module_struct_entry
val sexp_of_module_struct_entry : module_struct_entry -> Sexplib0.Sexp.t
type module_params_entry = (Names.MBId.t * module_struct_entry * inline) list
val module_params_entry_of_sexp : Sexplib0.Sexp.t -> module_params_entry
val sexp_of_module_params_entry : module_params_entry -> Sexplib0.Sexp.t
type module_entry = Entries.module_entry =
  1. | MType of module_params_entry * module_struct_entry
  2. | MExpr of module_params_entry * module_struct_entry * module_struct_entry option
val module_entry_of_sexp : Sexplib0.Sexp.t -> module_entry
val sexp_of_module_entry : module_entry -> Sexplib0.Sexp.t
type module_type_entry = module_params_entry * module_struct_entry
val module_type_entry_of_sexp : Sexplib0.Sexp.t -> module_type_entry
val sexp_of_module_type_entry : module_type_entry -> Sexplib0.Sexp.t
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