2023-04-11 13:49:22 +03:00
|
|
|
typeclass Copy =
|
|
|
|
|
& copy : Copy -> Copy
|
2023-03-31 12:10:12 +03:00
|
|
|
|
2023-04-11 13:49:22 +03:00
|
|
|
typeclass (Ord : #Eq) =
|
2023-04-29 12:33:05 +03:00
|
|
|
& is_less_then : Ord -> Bool
|
2023-03-31 12:10:12 +03:00
|
|
|
|
2023-04-11 13:49:22 +03:00
|
|
|
typeclass (D : #A #B #C) 'A 'B =
|
2023-03-31 12:10:12 +03:00
|
|
|
& do_something : Unit -> (& 'A & 'B)
|
|
|
|
|
|
2023-04-11 13:49:22 +03:00
|
|
|
typeclass E 'A =
|
2023-03-31 12:10:12 +03:00
|
|
|
& do_something : Unit -> 'A
|
|
|
|
|
|
2023-04-29 12:33:05 +03:00
|
|
|
decl ( == ) ('A : #Ord) : 'A -> 'A -> Bool
|
2023-05-07 09:25:38 +03:00
|
|
|
def ( == ) : a b = a.is_equal_to: b
|
2023-04-29 12:33:05 +03:00
|
|
|
|
|
|
|
|
decl ( < ) ('A : #Ord) : 'A -> 'A -> Bool
|
2023-05-07 09:25:38 +03:00
|
|
|
def ( < ) : a b = a.is_less_then: b
|
2023-04-29 12:33:05 +03:00
|
|
|
|
|
|
|
|
decl ( > ) ('A : #Ord) : 'A -> 'A -> Bool
|
|
|
|
|
def ( > ) : a b = !(a <= b)
|
|
|
|
|
|
|
|
|
|
decl ( <= ) ('A : #Ord) : 'A -> 'A -> Bool
|
|
|
|
|
def ( <= ) : a b = (a < b) || (a == b)
|
|
|
|
|
|
|
|
|
|
decl ( >= ) ('A : #Ord) : 'A -> 'A -> Bool
|
|
|
|
|
def ( >= ) : a b = !(a < b)
|