[Agda] Modelling term-rewriting systems in Agda

Jacques Carette carette at mcmaster.ca
Tue Oct 22 16:33:10 CEST 2013


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


More information about the Agda mailing list