[Agda] guardedness-preserving-type-constructors failing termination checker

Nils Anders Danielsson nad at cse.gu.se
Fri Sep 20 18:54:03 CEST 2013

On 2013-09-20 18:34, Twan van Laarhoven wrote:
> I was playing around with guardedness-preserving-type-constructors and
> ΠΣ style definitions; and some of the original examples no longer
> work. For instance the code at the bottom of
> https://lists.chalmers.se/pipermail/agda/2010/001720.html fails the
> termination checker.

The example doesn't work if ∃ is defined as in the standard library. It
should work if ∃ is replaced by Σ _.


More information about the Agda mailing list