[Agda] Modelling term-rewriting systems in Agda

[Jacques Carette]

On 2013-10-22 6:15 AM, Sergei Meshveliani wrote:
> 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.

Hello Sergei,

     Thanks for this, but I really am asking for something 
Agda-specific.  As you well know, going from Haskell to Agda is not 
straightforward, and what constitutes a 'good' set of encodings (data 
structures) in Haskell can be wildly different than the same in Agda.

     And this is exactly where I do not wish to re-invent.

Jacques