mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-22 03:01:31 +03:00
14 lines
200 B
Idris
14 lines
200 B
Idris
module Control.Ord
|
|
|
|
%default total
|
|
|
|
namespace Semigroup
|
|
|
|
public export
|
|
[Maximum] Ord a => Semigroup a where
|
|
(<+>) = max
|
|
|
|
public export
|
|
[Minimum] Ord a => Semigroup a where
|
|
(<+>) = min
|