[Agda] Possibly infinite/exponential compilation time by just calling a certain function

Nils Anders Danielsson nad at cse.gu.se
Wed Jun 28 11:41:04 CEST 2017


On 2017-06-27 17:09, Jan Bracker wrote:
> I tried to add the last postulate I need, but even though I now have
> marked all of the proofs as abstract the compilation time is again at
> 30+ minutes with no end in sight:

Some other things to try:

* Use copatterns to define records.

* Turn off η-equality for record types.

(I don't know if either of these things will help.)

-- 
/NAD


More information about the Agda mailing list