module Prelude.Algebra
import Builtins
infixl 6 <+>
%access public
--------------------------------------------------------------------------------
-- A modest class hierarchy
--------------------------------------------------------------------------------
||| Sets equipped with a single binary operation that is associative. Must
||| satisfy the following laws:
|||
||| + Associativity of `<+>`:
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
class Semigroup a where
(<+>) : a -> a -> a
||| Sets equipped with a single binary operation that is associative, along with
||| a neutral element for that binary operation. Must satisfy the following
||| laws:
|||
||| + Associativity of `<+>`:
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Neutral for `<+>`:
||| forall a, a <+> neutral == a
||| forall a, neutral <+> a == a
class Semigroup a => Monoid a where
neutral : a