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.11.0+0.11.1.tbz
sha256=f06bb0ab1041ac6f8d73faddda404827ce94b6b3310483e93d7fd18bd018e1ed
sha512=ecbed7b5b8451f65d40bf50fd1471b5038029c6f1ae8912c8cb51e61699cc4c158bc4f3533ec5f0898d1fc3d91683c0ff815fa44be7fdaedea59b71ca1d1b7d3

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

Module Serlib.Ser_names

module Id : sig ... end
module Name : SerType.SJ with type t = Names.Name.t
module DirPath : SerType.SJ with type t = Names.DirPath.t
module DPmap : Ser_cMap.ExtS with type key = DirPath.t and type 'a t = 'a Names.DPmap.t
module Label : SerType.S with type t = Names.Label.t
module MBId : SerType.S with type t = Names.MBId.t
module ModPath : SerType.S with type t = Names.ModPath.t
module MPmap : Ser_cMap.ExtS with type key = ModPath.t and type 'a t = 'a Names.MPmap.t
module KerName : SerType.S with type t = Names.KerName.t
module Constant : SerType.SJ with type t = Names.Constant.t
module Cmap : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Names.Cmap.t
module Cmap_env : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Names.Cmap_env.t
module MutInd : SerType.S with type t = Names.MutInd.t
module Mindmap : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Names.Mindmap.t
module Mindmap_env : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Names.Mindmap_env.t
type 'a tableKey = 'a Names.tableKey
val tableKey_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a tableKey
val sexp_of_tableKey : ('a -> Sexplib.Sexp.t) -> 'a tableKey -> Sexplib.Sexp.t
type variable = Names.variable
type inductive = Names.inductive
type constructor = Names.constructor
module Projection : sig ... end
module GlobRef : SerType.SJ with type t = Names.GlobRef.t
val variable_of_sexp : Sexplib.Sexp.t -> variable
val sexp_of_variable : variable -> Sexplib.Sexp.t
val inductive_of_sexp : Sexplib.Sexp.t -> inductive
val sexp_of_inductive : inductive -> Sexplib.Sexp.t
val inductive_of_yojson : Yojson.Safe.t -> (inductive, string) Result.result
val inductive_to_yojson : inductive -> Yojson.Safe.t
val constructor_of_sexp : Sexplib.Sexp.t -> constructor
val sexp_of_constructor : constructor -> Sexplib.Sexp.t
val constructor_of_yojson : Yojson.Safe.t -> (constructor, string) Result.result
val constructor_to_yojson : constructor -> Yojson.Safe.t
type evaluable_global_reference = Names.evaluable_global_reference
val evaluable_global_reference_of_sexp : Sexplib.Sexp.t -> evaluable_global_reference
val sexp_of_evaluable_global_reference : evaluable_global_reference -> Sexplib.Sexp.t
type lident = Names.lident
val lident_of_sexp : Sexplib.Sexp.t -> lident
val sexp_of_lident : lident -> Sexplib.Sexp.t
val lident_of_yojson : Yojson.Safe.t -> (lident, string) Result.result
val lident_to_yojson : lident -> Yojson.Safe.t
type lname = Names.lname
val lname_of_sexp : Sexplib.Sexp.t -> lname
val sexp_of_lname : lname -> Sexplib.Sexp.t
val lname_of_yojson : Yojson.Safe.t -> (lname, string) Result.result
val lname_to_yojson : lname -> Yojson.Safe.t
type lstring = Names.lstring
val lstring_of_sexp : Sexplib.Sexp.t -> lstring
val sexp_of_lstring : lstring -> Sexplib.Sexp.t
val lstring_of_yojson : Yojson.Safe.t -> (lstring, string) Result.result
val lstring_to_yojson : lstring -> Yojson.Safe.t