[Agda] complex indices

Brandon Moore brandon_m_moore at yahoo.com
Wed Feb 22 21:59:26 CET 2012

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

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

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

More information about the Agda mailing list