[Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

Cody Roux cody.roux at andrew.cmu.edu
Mon Jan 6 17:54:07 CET 2014


Nice summary!


On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
> Agda enforces termination via a termination checker which is more 
> flexible but I think less principled than Coq's approach. 
     That's a bit scary given that there was an inconsistency found in 
the Coq termination checker just a couple of weeks ago :)

     BTW, has anyone tried reproducing the bug in Agda?


Cody


More information about the Agda mailing list