90bfd84a07
In the standard library, we should use explicit universe variables for universe polymorphic definitions. Users that want to declare universe polymorphic definitions but do not want to provide universe level parameters should use Type _ or Type*
74 lines
3 KiB
Text
74 lines
3 KiB
Text
alternative : (Type → Type) → Type₂
|
|
applicative : (Type → Type) → Type₂
|
|
decidable : Prop → Type
|
|
functor : (Type → Type) → Type₂
|
|
has_add : Type u → Type (max 1 u)
|
|
has_andthen : Type u → Type (max 1 u)
|
|
has_append : Type u → Type (max 1 u)
|
|
has_coe : Type u → Type v → Type (max 1 (imax u v))
|
|
has_coe_t : Type u → Type v → Type (max 1 (imax u v))
|
|
has_coe_to_fun : Type u → Type (max (imax u v) (v+1))
|
|
has_coe_to_sort : Type u → Type (max (imax u v) (v+1))
|
|
has_div : Type u → Type (max 1 u)
|
|
has_dvd : Type u → Type (max 1 u)
|
|
has_inv : Type u → Type (max 1 u)
|
|
has_le : Type u → Type (max 1 u)
|
|
has_lift : Type u → Type v → Type (max 1 (imax u v))
|
|
has_lift_t : Type u → Type v → Type (max 1 (imax u v))
|
|
has_lt : Type u → Type (max 1 u)
|
|
has_mod : Type u → Type (max 1 u)
|
|
has_mul : Type u → Type (max 1 u)
|
|
has_neg : Type u → Type (max 1 u)
|
|
has_one : Type u → Type (max 1 u)
|
|
has_ordering : Type → Type
|
|
has_sizeof : Type u → Type (max 1 u)
|
|
has_sub : Type u → Type (max 1 u)
|
|
has_to_format : Type u → Type (max 1 u)
|
|
has_to_pexpr : Type u → Type (max 1 u)
|
|
has_to_string : Type u → Type (max 1 u)
|
|
has_to_tactic_format : Type → Type
|
|
has_zero : Type u → Type (max 1 u)
|
|
inhabited : Type u → Type (max 1 u)
|
|
is_associative : Π {A : Type u}, (A → A → A) → Type
|
|
monad : (Type → Type) → Type₂
|
|
nonempty : Type u → Prop
|
|
point : Type u_1 → Type u_2 → Type (max 1 u_1 u_2)
|
|
setoid : Type u → Type (max 1 u)
|
|
subsingleton : Type u → Prop
|
|
alternative : (Type → Type) → Type₂
|
|
applicative : (Type → Type) → Type₂
|
|
decidable : Prop → Type
|
|
functor : (Type → Type) → Type₂
|
|
has_add : Type u → Type (max 1 u)
|
|
has_andthen : Type u → Type (max 1 u)
|
|
has_append : Type u → Type (max 1 u)
|
|
has_coe : Type u → Type v → Type (max 1 (imax u v))
|
|
has_coe_t : Type u → Type v → Type (max 1 (imax u v))
|
|
has_coe_to_fun : Type u → Type (max (imax u v) (v+1))
|
|
has_coe_to_sort : Type u → Type (max (imax u v) (v+1))
|
|
has_div : Type u → Type (max 1 u)
|
|
has_dvd : Type u → Type (max 1 u)
|
|
has_inv : Type u → Type (max 1 u)
|
|
has_le : Type u → Type (max 1 u)
|
|
has_lift : Type u → Type v → Type (max 1 (imax u v))
|
|
has_lift_t : Type u → Type v → Type (max 1 (imax u v))
|
|
has_lt : Type u → Type (max 1 u)
|
|
has_mod : Type u → Type (max 1 u)
|
|
has_mul : Type u → Type (max 1 u)
|
|
has_neg : Type u → Type (max 1 u)
|
|
has_one : Type u → Type (max 1 u)
|
|
has_ordering : Type → Type
|
|
has_sizeof : Type u → Type (max 1 u)
|
|
has_sub : Type u → Type (max 1 u)
|
|
has_to_format : Type u → Type (max 1 u)
|
|
has_to_pexpr : Type u → Type (max 1 u)
|
|
has_to_string : Type u → Type (max 1 u)
|
|
has_to_tactic_format : Type → Type
|
|
has_zero : Type u → Type (max 1 u)
|
|
inhabited : Type u → Type (max 1 u)
|
|
is_associative : Π {A : Type u}, (A → A → A) → Type
|
|
monad : (Type → Type) → Type₂
|
|
nonempty : Type u → Prop
|
|
point : Type u_1 → Type u_2 → Type (max 1 u_1 u_2)
|
|
setoid : Type u → Type (max 1 u)
|
|
subsingleton : Type u → Prop
|