Sorts (u.3758aa3ddc38cffa23da0eeb3fa7893a.rocq-runtime.9.0.0.doc.rocq-runtime.kernel.Sorts)

The sorts of CCI.

Sourcetype family =

| InSProp
| InProp
| InSet
| InType
| InQSort

Sourceval all_families : family list

Sourcemodule QVar : sig ... end

Sourcemodule Quality : sig ... end

Sourcemodule QConstraint : sig ... end

Sourcemodule QConstraints : sig ... end

Source

val enforce_eq_quality : 
  Quality.t ->
  Quality.t ->
  QConstraints.t ->
  QConstraints.t

Source

val enforce_leq_quality : 
  Quality.t ->
  Quality.t ->
  QConstraints.t ->
  QConstraints.t

Sourcemodule QUConstraints : sig ... end

Sourcetype t = private

| SProp
| Prop
| Set
| Type of Univ.Universe.t
| QSort of QVar.t * Univ.Universe.t

Sourceval sprop : t

Sourceval set : t

Sourceval prop : t

Sourceval type1 : t

Sourceval qsort : QVar.t -> Univ.Universe.t -> t

Sourceval make : Quality.t -> Univ.Universe.t -> t

Sourceval equal : t -> t -> bool

Sourceval compare : t -> t -> int

Sourceval hash : t -> int

Sourceval is_sprop : t -> bool

Sourceval is_set : t -> bool

Sourceval is_prop : t -> bool

Sourceval is_small : t -> bool

Sourceval family : t -> family

Sourceval quality : t -> Quality.t

Sourceval hcons : t -> t

Sourceval family_compare : family -> family -> int

Sourceval family_equal : family -> family -> bool

Sourceval family_leq : family -> family -> bool

Sourceval sort_of_univ : Univ.Universe.t -> t

Sourceval levels : t -> Univ.Level.Set.t

Sourceval super : t -> t

Source

val subst_fn : 
  ((QVar.t -> Quality.t) * (Univ.Universe.t -> Univ.Universe.t)) ->
  t ->
  t

Sourcetype relevance =

| Relevant
| Irrelevant
| RelevanceVar of QVar.t

On binders: is this variable proof relevant

Sourceval relevance_hash : relevance -> int

Sourceval relevance_equal : relevance -> relevance -> bool

Sourceval relevance_subst_fn : (QVar.t -> Quality.t) -> relevance -> relevance

Sourceval relevance_of_sort : t -> relevance

Sourceval relevance_of_sort_family : family -> relevance

Sourceval debug_print : t -> Pp.t

Sourceval pr_sort_family : family -> Pp.t

Sourcetype pattern =

| PSProp
| PSSProp
| PSSet
| PSType of int option
| PSQSort of int option * int option

Source

val pattern_match : 
  pattern ->
  t ->
  ('t, Quality.t, Univ.Level.t) Partial_subst.t ->
  ('t, Quality.t, Univ.Level.t) Partial_subst.t option