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

[Nils Anders Danielsson]

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 Σ _.

-- 
/NAD