forked from GitHub/gf-core
Transfer: Ord extends Eq.
This commit is contained in:
@@ -90,7 +90,8 @@ data Ordering : Type where
|
|||||||
GT : Ordering
|
GT : Ordering
|
||||||
|
|
||||||
Ord : Type -> Type
|
Ord : Type -> Type
|
||||||
Ord A = sig { compare : A -> A -> Ordering }
|
Ord A = sig eq : A -> A -> Bool
|
||||||
|
compare : A -> A -> Ordering
|
||||||
|
|
||||||
compare : (A : Type) -> Ord A -> A -> A -> Ordering
|
compare : (A : Type) -> Ord A -> A -> A -> Ordering
|
||||||
compare _ d = d.compare
|
compare _ d = d.compare
|
||||||
|
|||||||
Reference in New Issue
Block a user