[Agda] Modelling term-rewriting systems in Agda

[Sergei Meshveliani]

On Tue, 2013-10-22 at 09:22 -0400, Jacques Carette wrote:
> 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


Do you mean
  to formulate in Agda 
  1) a notion of what is a set of _rewriting rules_
     (or `equations'),
  2) a notion of a rule (equation) set being confluent,
  and so on
?

------
Sergei