[Agda] Modelling term-rewriting systems in Agda

[Jacques Carette]

On 2013-10-22 8:50 AM, Sergei Meshveliani wrote:
> On Tue, 2013-10-22 at 14:15 +0400, Sergei Meshveliani wrote:
> I am not sure that I understand the goal:
>> where you also prove properties like confluence (using critical
>> pairs)?
>

That was sloppy writing on my part: I mean exactly what you said. What I 
wanted to convey is that confluence and critical pairs will be important 
ingredients, so I need to understand how to represent these concepts in 
convenient ways.  "representing concepts in convenient ways" is often a 
rather non-trivial question in dependently-typed settings.

Jacques