[Agda] Understanding productivity

Nils Anders Danielsson nad at chalmers.se
Mon Nov 5 10:49:44 CET 2012

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


> [...] 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

This explanation ignores size-change termination.


More information about the Agda mailing list