[Agda] complex indices

[Ramana Kumar]

Yes but I think the return type in my example was Set.
Note, for example, that this is allowed:

  bar : Bool → Set1
  bar b = Set

  data foo : let x = true in bar x where
    baz : foo

Maybe it shouldn't be?

2012/2/22 Peter Dybjer <peterd at chalmers.se>

> Ramana,
>
> When you use data you define a (family of) sets, hence the return type
> should always be Set.
>
> Cheers, Peter (back in Sweden)
>
> ________________________________________
> From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] on
> behalf of Ramana Kumar [rk436 at cam.ac.uk]
> Sent: Wednesday, February 22, 2012 9:34 PM
> To: agda at lists.chalmers.se
> Subject: [Agda] complex indices
>
> Why exactly does this fail?
> Should it?
>
> data foo : (y : Bool) → if y then Set else Set where
>  bar : foo true Bool
>
> The error I get is
>
> if @0 then Set else Set != Set of type Set₁
> when checking the definition of foo
>
> which is a little cryptic (but probably no more so than my declaration).
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120222/217fe64f/attachment.html