On 2013-10-22 10:24 AM, Sergei Meshveliani wrote: > 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 > ? Yes. And to be able to effectively work with these notions. Just encoding is easy enough. Jacques