IdrisDoc: Prelude.Algebra

# Prelude.Algebra

interface Monoid

  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
  neutral : Monoid ty => ty
interface Semigroup

  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
  (<+>) : Semigroup ty => ty -> ty -> ty
    Fixity
      Left associative, precedence 6