package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t

A universe instance represents a vector of argument universes and sort qualities to a polymorphic definition (constant, inductive or constructor).

val empty : t
val is_empty : t -> bool
val of_array : (Sorts.Quality.t array * Univ.Level.t array) -> t
val to_array : t -> Sorts.Quality.t array * Univ.Level.t array
val abstract_instance : (int * int) -> t

Instance of the given size made of QVar/Level.var

val append : t -> t -> t

To concatenate two instances, used for discharge

val equal : t -> t -> bool

Equality

val length : t -> int * int

Instance length

val hcons : t -> t

Hash-consing.

val hash : t -> int

Hash value

val share : t -> t * int

Simultaneous hash-consing and hash-value computation

val pr : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t

Pretty-printing, no comments

The set of levels in the instance

val subst_fn : ((Sorts.QVar.t -> Sorts.Quality.t) * (Univ.Level.t -> Univ.Level.t)) -> t -> t
type mask = Sorts.Quality.pattern array * int option array
val pattern_match : mask -> t -> ('term, Sorts.Quality.t, Univ.Level.t) Partial_subst.t -> ('term, Sorts.Quality.t, Univ.Level.t) Partial_subst.t option

Pattern matching, as used by the rewrite rules mechanism

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