Module PConstraints

type pconstraints = t

Stands for prenex sort poly constraints

val empty : t
val is_empty : t -> bool
val equal : t -> t -> bool
val qualities : t -> Sorts.ElimConstraints.t
val univs : t -> Univ.UnivConstraints.t
val of_qualities : Sorts.ElimConstraints.t -> t
val of_univs : Univ.UnivConstraints.t -> t
val set_qualities : Sorts.ElimConstraints.t -> t -> t
val set_univs : Univ.UnivConstraints.t -> t -> t
val add_quality : Sorts.ElimConstraint.t -> t -> t
val add_univ : Univ.UnivConstraint.t -> t -> t
val union : t -> t -> t
val diff : t -> t -> t
val elements : t -> Sorts.ElimConstraint.t list * Univ.UnivConstraint.t list
val filter_qualities : (Sorts.ElimConstraints.elt -> bool) -> t -> t
val filter_univs : (Univ.UnivConstraints.elt -> bool) -> t -> t
val pr : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> t -> Pp.t
val hcons : t Hashcons.f
type 'a constrained = 'a * t
val constraints_of : 'a constrained -> t
type 'a constraint_function = 'a -> 'a -> t -> t
val enforce_eq_univ : Univ.Level.t constraint_function
val enforce_leq_univ : Univ.Level.t constraint_function
val enforce_eq_quality : Sorts.Quality.t constraint_function
val enforce_elim_to : Sorts.Quality.t constraint_function
val fold : ((Sorts.ElimConstraint.t -> 'a -> 'a) * (Univ.UnivConstraint.t -> 'b -> 'b)) -> t -> ('a * 'b) -> 'a * 'b

Polymorphic contexts (as sets)

A set of qualities and universes with polymorphic PConstraints.t. We linearize the set to a list after typechecking. Beware, representation could change.

module ContextSet : sig ... end
type 'a in_poly_context_set = 'a * ContextSet.t