package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Level : SerType.SJHC with type t = Univ.Level.t
module Universe : SerType.SJHC with type t = Univ.Universe.t
module Variance : SerType.SJHC with type t = Univ.Variance.t
module Instance : SerType.SJHC with type t = Univ.Instance.t
type constraint_type = Univ.constraint_type
val sexp_of_constraint_type : constraint_type -> Sexplib0.Sexp.t
val constraint_type_of_sexp : Sexplib0.Sexp.t -> constraint_type
val constraint_type_to_yojson : constraint_type -> Yojson.Safe.t
val hash_fold_constraint_type : Base.Hash.state -> constraint_type -> Base.Hash.state
val hash_constraint_type : constraint_type -> Base.Hash.hash_value
val compare_constraint_type : constraint_type -> constraint_type -> int
type univ_constraint = Univ.univ_constraint
val univ_constraint_of_sexp : Sexplib.Sexp.t -> univ_constraint
val sexp_of_univ_constraint : univ_constraint -> Sexplib.Sexp.t
module UContext : SerType.SJHC with type t = Univ.UContext.t
type 'a in_universe_context = 'a Univ.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 in_universe_context_set = 'a Univ.in_universe_context_set
val in_universe_context_set_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a in_universe_context_set
val sexp_of_in_universe_context_set : ('a -> Sexplib.Sexp.t) -> 'a in_universe_context_set -> Sexplib.Sexp.t
type 'a puniverses = 'a * Instance.t
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 puniverses_to_yojson : ('a -> Yojson.Safe.t) -> 'a puniverses -> Yojson.Safe.t
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
type explanation = Univ.explanation
val explanation_of_sexp : Sexplib.Sexp.t -> explanation
val sexp_of_explanation : explanation -> 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