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

Andreas Abel andreas.abel at ifi.lmu.de
Fri Sep 20 20:48:40 CEST 2013

On 20.09.2013 18:54, Nils Anders Danielsson wrote:
> 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 Σ _.

For the same reason, the version with if_then_else_ is refuted.  These 
functions (\exists, if) are not inlined before termination checking. 
But then, since they are treated as arbitrary functions, they destroy 

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list