package rocq-runtime

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

Module UnivGen.QualityOrSetSource

Sourcetype t =
  1. | Qual of Sorts.Quality.t
  2. | Set
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval of_quality : Sorts.Quality.t -> t
Sourceval of_sort : Sorts.t -> t
Sourceval quality : t -> Sorts.Quality.t
Sourceval eliminates_to : t -> t -> bool
Sourceval set : t
Sourceval qtype : t
Sourceval prop : t
Sourceval sprop : t
Sourceval is_type : t -> bool
Sourceval is_set : t -> bool
Sourceval is_prop : t -> bool
Sourceval is_sprop : t -> bool
Sourceval pr : (Sorts.QVar.t -> Pp.t) -> t -> Pp.t
Sourceval raw_pr : t -> Pp.t
Sourceval all_constants : t list
Sourceval all : t list