
  0 | module Algebra.Monoid
  1 | 
  2 | import Data.List
  3 | 
  4 | %default total
  5 | 
  6 | ||| This interface is a witness that for a
  7 | ||| type `a` the axioms of a monoid hold: `(<+>)` is associative
  8 | ||| with `neutral` being the neutral element.
  9 | public export
 10 | interface Monoid a => LMonoid a where
 11 |   0 appendAssociative : {x,y,z : a} -> x <+> (y <+> z) === (x <+> y) <+> z
 12 | 
 13 |   0 appendLeftNeutral : {x : a} -> Prelude.neutral <+> x === x
 14 | 
 15 |   0 appendRightNeutral : {x : a} -> x <+> Prelude.neutral === x
 16 | 
 17 | export
 18 | LMonoid (List a) where
 19 |   appendAssociative = Data.List.appendAssociative _ _ _
 20 |   appendRightNeutral = appendNilRightNeutral _
 21 |   appendLeftNeutral = Refl
 22 | 
 23 | unsafeRefl : a === b
 24 | unsafeRefl = believe_me (Refl {x = a})
 25 | 
 26 | export
 27 | LMonoid String where
 28 |   appendAssociative = unsafeRefl
 29 |   appendRightNeutral = unsafeRefl
 30 |   appendLeftNeutral = unsafeRefl
 31 | 
 32 | ||| This interface is a witness that for a
 33 | ||| type `a` the axioms of a commutative monoid hold:
 34 | ||| `(<+>)` is commutative.
 35 | public export
 36 | interface LMonoid a => CommutativeMonoid a where
 37 |   0 appendCommutative : {x,y : a} -> x <+> y === y <+> x
 38 |