package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Names = Ser_names
module Evar = Ser_evar
module Sorts = Ser_sorts
module Constr = Ser_constr
module Univ = Ser_univ
type t = t -> t
val t_of_sexp : Sexplib0.Sexp.t -> t
val sexp_of_t : t -> Sexplib0.Sexp.t
type tag = int
val tag_of_sexp : Sexplib0.Sexp.t -> tag
val sexp_of_tag : tag -> Sexplib0.Sexp.t
type arity = int
val arity_of_sexp : Sexplib0.Sexp.t -> arity
val sexp_of_arity : arity -> Sexplib0.Sexp.t
type reloc_table = (tag * arity) array
val reloc_table_of_sexp : Sexplib0.Sexp.t -> reloc_table
val sexp_of_reloc_table : reloc_table -> Sexplib0.Sexp.t
type annot_sw = Nativevalues.annot_sw = {
  1. asw_ind : Names.inductive;
  2. asw_ci : Constr.case_info;
  3. asw_reloc : reloc_table;
  4. asw_finite : bool;
  5. asw_prefix : string;
}
val annot_sw_of_sexp : Sexplib0.Sexp.t -> annot_sw
val sexp_of_annot_sw : annot_sw -> Sexplib0.Sexp.t
type symbol = Nativevalues.symbol =
  1. | SymbValue of t
  2. | SymbSort of Sorts.t
  3. | SymbName of Names.Name.t
  4. | SymbConst of Names.Constant.t
  5. | SymbMatch of annot_sw
  6. | SymbInd of Names.inductive
  7. | SymbMeta of Constr.metavariable
  8. | SymbEvar of Evar.t
  9. | SymbLevel of Univ.Level.t
  10. | SymbProj of Names.inductive * int
val symbol_of_sexp : Sexplib0.Sexp.t -> symbol
val sexp_of_symbol : symbol -> Sexplib0.Sexp.t
type symbols = symbol array
val symbols_of_sexp : Sexplib0.Sexp.t -> symbols
val sexp_of_symbols : symbols -> 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