[Agda] Modelling term-rewriting systems in Agda

[Sergei Meshveliani]

On Mon, 2013-10-21 at 16:42 -0400, Jacques Carette wrote:
> Hello all,
>      Does anyone have an example of modelling a term rewriting system, 
> where you also prove properties like confluence (using critical pairs)?  
> I am about to do this, and I would much rather use "best practices" 
> rather than muddle my way through via re-inventing squarish wheels.
> 
> Jacques

I have the  Dumatel  library for this, written in  Haskell.

It has  critical pairs, unfailing completion, modulo AC also,
and other useful things, in a very general setting.
This is for  _many-sorted term rewriting_.
(It also has inductive prover function).

The last version project is interrupted, is not workable
(it has polymorphic sorts evaluated dynamically, and I have met
technical difficulties).

But if you ask, I can send you an older version, which has working 
(AC) completion.
I have an hope that  Dumatel  can be modified and used as a library
prover helping to write proofs in Agda programs.

Regards,

------
Sergei