[Agda] no longer type checks

[Nils Anders Danielsson]

On 2012-12-20 00:14, Andreas Abel wrote:
> So 1. we analyze the situation at the time of a data definition (which
> constructor parameters are to be treated as indices in 2. the pattern
> matching situation), and at 2. pattern matching time we analyse the
> index expressions taking into account constructor indices and
> constructor parameters counted as indices according to 1.

I think you mean "constructor arguments" rather than "constructor
indices".

-- 
/NAD