[Agda] Understanding productivity

[Nils Anders Danielsson]

On 2012-11-02 23:20, Daniel Peebles wrote:
> I've been experimenting with more constructive definitions of
> Data.Nat.InfinitelyOften for some experiments with primality.

I have some definitions in

   http://www.cse.chalmers.se/~nad/listings/codata/InfinitelyOften.html.

> [...] I don't understand what conditions it's using to figure it out.

There is a simplified explanation in the following paper (Section 2.5):

   Subtyping, Declaratively
   An Exercise in Mixed Induction and Coinduction
   Nils Anders Danielsson and Thorsten Altenkirch
   http://www.cse.chalmers.se/~nad/publications/danielsson-altenkirch-subtyping.html

This explanation ignores size-change termination.

-- 
/NAD