Documentation
Init
.
Data
.
Subtype
.
OrderExtra
Search
return to top
source
Imports
Init.Data.Ord.Basic
Init.Data.Subtype.Order
Imported by
instOrdSubtype
source
instance
instOrdSubtype
{
α
:
Type
u}
[
Ord
α
]
{
P
:
α
→
Prop
}
:
Ord
(
Subtype
P
)
Equations