package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a in_universe_context = 'a UVars.in_universe_context

A value in a universe context (resp. context set).

val in_universe_context_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a in_universe_context
val sexp_of_in_universe_context : ('a -> Sexplib.Sexp.t) -> 'a in_universe_context -> Sexplib.Sexp.t
type 'a puniverses = 'a * Instance.t
val puniverses_to_yojson : ('a -> Yojson.Safe.t) -> 'a puniverses -> Yojson.Safe.t
val puniverses_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a puniverses Ppx_deriving_yojson_runtime.error_or
val sexp_of_puniverses : ('a -> Sexplib0.Sexp.t) -> 'a puniverses -> Sexplib0.Sexp.t
val puniverses_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a puniverses
val hash_fold_puniverses : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a puniverses -> Base.Hash.state
val compare_puniverses : ('a -> 'a -> int) -> 'a puniverses -> 'a puniverses -> int
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