Module SortsSource

The sorts of CCI.
Sourcetype family =
  1. | InSProp
  2. | InProp
  3. | InSet
  4. | InType
Sourceval all_families : family list
Sourcetype t = private
  1. | SProp
  2. | Prop
  3. | Set
  4. | Type of Univ.Universe.t
Sourceval sprop : t
Sourceval set : t
Sourceval prop : t
Sourceval type1 : 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 hcons : t -> t
Sourceval family_compare : family -> family -> int
Sourceval family_equal : family -> family -> bool
Sourceval family_leq : family -> family -> bool
Sourceval univ_of_sort : t -> Univ.Universe.t
Sourceval sort_of_univ : Univ.Universe.t -> t
Sourceval super : t -> t
Sourcetype relevance =
  1. | Relevant
  2. | Irrelevant

On binders: is this variable proof relevant

Sourceval relevance_hash : relevance -> int
Sourceval relevance_equal : relevance -> relevance -> bool
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