[Agda-dev] without K and termination

[Nils Anders Danielsson]

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