[Agda-dev] without K and termination

[John Leo]

Hi Nils,

Thanks very much! That does indeed look like it should be the same
underlying problem. I've added this example to 2890.

John

On Tue, Mar 20, 2018 at 3:58 AM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2018-03-16 19:33, John Leo wrote:
>
>> This seems to be some strange interplay between records, with clauses,
>> and without-K, but I don't know if this is a bug or just some subtlety
>> that I don't understand. Please let me know what you think, and if
>> it's a bug I'm happy to file it.
>>
>
> Perhaps your problem is related to the following set of issues:
>
>   https://github.com/agda/agda/issues/1023
>   https://github.com/agda/agda/issues/1680
>   https://github.com/agda/agda/issues/2890
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20180320/d251cc34/attachment.html>