Yes but I think the return type in my example was Set.<br>Note, for example, that this is allowed:<br><br> bar : Bool → Set1<br> bar b = Set<br><br> data foo : let x = true in bar x where<br> baz : foo<br><br>Maybe it shouldn't be?<br>
<br><div class="gmail_quote">2012/2/22 Peter Dybjer <span dir="ltr"><<a href="mailto:peterd@chalmers.se">peterd@chalmers.se</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Ramana,<br>
<br>
When you use data you define a (family of) sets, hence the return type should always be Set.<br>
<br>
Cheers, Peter (back in Sweden)<br>
<br>
________________________________________<br>
From: <a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.se</a> [<a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.se</a>] on behalf of Ramana Kumar [<a href="mailto:rk436@cam.ac.uk">rk436@cam.ac.uk</a>]<br>
Sent: Wednesday, February 22, 2012 9:34 PM<br>
To: <a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
Subject: [Agda] complex indices<br>
<div class="HOEnZb"><div class="h5"><br>
Why exactly does this fail?<br>
Should it?<br>
<br>
data foo : (y : Bool) → if y then Set else Set where<br>
bar : foo true Bool<br>
<br>
The error I get is<br>
<br>
if @0 then Set else Set != Set of type Set₁<br>
when checking the definition of foo<br>
<br>
which is a little cryptic (but probably no more so than my declaration).<br>
</div></div></blockquote></div><br>