Hi,<br><br>You should omit the type in the 'definition' of B:<div><br></div><div><div>data B : Set</div><div><br></div><div>data A : Set where</div><div> bA : B → A</div><div><br></div><div>data B where</div><div> aB : A → B</div><div> b : B</div></div><div><br></div><div>James</div><div><br></div><br><div class="gmail_quote">On Tue Jan 27 2015 at 10:50:47 AM Dominique Devriese <<a href="mailto:dominique.devriese@cs.kuleuven.be">dominique.devriese@cs.kuleuven.be</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all,<br>
<br>
Can anyone tell me if the following is supposed to work, or if I<br>
should use old-style mutual blocks for this? Or maybe I've forgotten<br>
something else? I currently get an error about a missing definition<br>
for B.<br>
<br>
data B : Set<br>
<br>
data A : Set where<br>
bA : B → A<br>
<br>
data B : Set where<br>
aB : A → B<br>
b : B<br>
<br>
Thanks,<br>
Dominique<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div>