package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Serlib.Ser_univSource

Sourcemodule Level : SerType.SJ with type t = Univ.Level.t
Sourcemodule Universe : SerType.SJ with type t = Univ.Universe.t
Sourcemodule Variance : SerType.SJ with type t = Univ.Variance.t
Sourcemodule Instance : SerType.SJ with type t = Univ.Instance.t
Sourcetype constraint_type = Univ.constraint_type
Sourceval constraint_type_of_sexp : Sexplib.Sexp.t -> constraint_type
Sourceval sexp_of_constraint_type : constraint_type -> Sexplib.Sexp.t
Sourceval constraint_type_of_yojson : Yojson.Safe.t -> (constraint_type, string) Result.result
Sourceval constraint_type_to_yojson : constraint_type -> Yojson.Safe.t
Sourcetype univ_constraint = Univ.univ_constraint
Sourceval univ_constraint_of_sexp : Sexplib.Sexp.t -> univ_constraint
Sourceval sexp_of_univ_constraint : univ_constraint -> Sexplib.Sexp.t
Sourcemodule Constraint : SerType.SJ with type t = Univ.Constraint.t
Sourcemodule UContext : SerType.S with type t = Univ.UContext.t
Sourcemodule AUContext : SerType.S with type t = Univ.AUContext.t
Sourcemodule ContextSet : SerType.SJ with type t = Univ.ContextSet.t
Sourcetype 'a in_universe_context = 'a Univ.in_universe_context

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

Sourceval in_universe_context_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a in_universe_context
Sourceval sexp_of_in_universe_context : ('a -> Sexplib.Sexp.t) -> 'a in_universe_context -> Sexplib.Sexp.t
Sourcetype 'a in_universe_context_set = 'a Univ.in_universe_context_set
Sourceval in_universe_context_set_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a in_universe_context_set
Sourceval sexp_of_in_universe_context_set : ('a -> Sexplib.Sexp.t) -> 'a in_universe_context_set -> Sexplib.Sexp.t
Sourcetype 'a puniverses = 'a * Instance.t
Sourceval puniverses_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a puniverses
Sourceval sexp_of_puniverses : ('a -> Sexplib.Sexp.t) -> 'a puniverses -> Sexplib.Sexp.t
Sourceval puniverses_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a puniverses, string) Result.result
Sourceval puniverses_to_yojson : ('a -> Yojson.Safe.t) -> 'a puniverses -> Yojson.Safe.t
Sourcetype explanation = Univ.explanation
Sourceval explanation_of_sexp : Sexplib.Sexp.t -> explanation
Sourceval sexp_of_explanation : explanation -> Sexplib.Sexp.t
Sourcetype univ_inconsistency = Univ.univ_inconsistency
Sourceval univ_inconsistency_of_sexp : Sexplib.Sexp.t -> univ_inconsistency
Sourceval sexp_of_univ_inconsistency : univ_inconsistency -> Sexplib.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