[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