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

[Andreas Abel]

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 
guardedness.

-- 
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
http://www2.tcs.ifi.lmu.de/~abel/