[Agda] guardedness-preserving-type-constructors failing
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