[Agda] Coinductive indices

Nils Anders Danielsson nad at chalmers.se
Tue Mar 15 23:17:11 CET 2011


On 2011-03-15 22:21, Robert J. Simmons wrote:
> I'm not quite sure I understand the intuition, but as far as
> pattern-matching goes, it works beautifully. Thanks!

The delay constructor ♯_ is generative (any two copies are distinct) so
you should avoid mentioning it in type signatures.

-- 
/NAD



More information about the Agda mailing list