package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val make : Level.t -> t
val pr : t -> Pp.t
val pr_with : (Level.t -> Pp.t) -> t -> Pp.t
val is_level : t -> bool
val is_levels : t -> bool
val level : t -> Level.t option
val levels : t -> LSet.t
val super : t -> t
val sup : t -> t -> t
val sprop : t
val type0m : t
val type0 : t
val type1 : t
val is_sprop : t -> bool
val is_type0m : t -> bool
val is_type0 : t -> bool
val exists : ((Level.t * int) -> bool) -> t -> bool
val for_all : ((Level.t * int) -> bool) -> t -> bool
val repr : t -> (Level.t * int) list
module Set : sig ... end
module Map : sig ... end