[Agda] complex indices

[Brandon Moore]

Hello Ramana

Could you motivate your definition a bit more?
I don't have much idea what it should mean.
It seems very similar to a this definition,
which I am not surprised to see rejected

data foo : (y : Bool) -> Bool where

-- no constructors

If the idea is to have an inductive family where some indices
live at different levels, you might compare to this definition:

data foo : (y : Bool) → Set (if y then zero else suc zero) where
  bar : foo true

which produces a more straightforward error message

home/brandon/test/test.agda:5,6-9
The sort of foo cannot depend on its indices in the type (y : Bool)
→ Set (if y then zero else suc zero)
when checking the definition of foo

Brandon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120222/4e13b288/attachment.html