idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 13:11:30 +03:00
Code Issues Projects Releases Wiki Activity

[ prelude ] Implement Semigroup for ordinary pairs

Browse Source
This commit is contained in:
Denis Buzdalov 2021-09-03 16:39:22 +03:00 committed by G. Allais
parent 257783275e
commit 5d70c746b1
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/prelude/Prelude/Interfaces.idr
View File

@ -44,6 +44,14 @@ public export
Monoid () where Monoid () where
neutral = () neutral = ()
public export
Semigroup a => Semigroup b => Semigroup (a, b) where
(x, y) <+> (v, w) = (x <+> v, y <+> w)
public export
Monoid a => Monoid b => Monoid (a, b) where
neutral = (neutral, neutral)
public export public export
Semigroup Ordering where Semigroup Ordering where
LT <+> _ = LT LT <+> _ = LT