[Agda] non-constructor indices

[James Chapman]

Hi,

I don't think it should panic. It looks like you have found a bug in  
the (brand new) coverage checker.

You should raise it here:

http://code.google.com/p/agda/issues/list

In the meantime you can turn off the coverage checker by putting this  
at the top of you file:

{-# OPTIONS --no-coverage-check #-}

You can also turn it off on the command line if you want if you're  
using agda in batch mode.

$agda --no-coverage-check Bug.agda

You first version is accepted then.

This isn't an authoritative answer (I'm not an agda developer) but I  
hope it helps anyway.

Cheers,

James


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.