[Agda] how to use monoid solver and how to derive a concept monoid if assume we do not know monoid

[Mandy Martino]

Hi ,
i find many places  define  identity, symmetric and  transitive,   how to  use  monoid  solve and  which  can  it  solve?
i would like  to define a new  set  of  equivalence relations,  is  there  a  light  weight  version of  monoid?
assume we do not know monoid,  how to build  a concept such as  monoid  based  on  custom  equivalence  relations?
does  new  custom equivalence  relations  mainly  use  for  a  new kind of polynomials  algebra  and  Natural  number  system?
if so,  does it mean that  i edit  transitive  in  files which  have  transitive and  then  recompile  std-library  of  agda, then  it will work?

https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Algebra/Monoid-solver.agda
https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Relation/Binary/PropositionalEquality/Core.agda
https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Relation/Binary/Indexed/Core.agda

i find this  http://ocvs.cfv.jp/Agda/big-examples.alfa

Regards,
Martin  		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151214/3ab29cba/attachment.html