[Agda] Modelling term-rewriting systems in Agda

Jacques Carette carette at mcmaster.ca
Mon Oct 21 22:42:20 CEST 2013

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.


More information about the Agda mailing list