<div dir="ltr">The following seems to work:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">data Foo : Set<br>data Bar : Foo → Set<br>data Bar2 : Foo → Set<br><br>bar2-temp : (x : Foo) → Bar2 x<br><br>data Foo where<br> foo : (x : Foo) → Bar x → Bar2 x → Foo<br><br>data Bar where<br> bar : (x : Foo) → Bar x<br> bar' : (x : Foo) → Bar (foo x (bar x) (bar2-temp x))<br><br>data Bar2 where<br> bar2 : (x : Foo) → Bar2 x<br> bar2' : (x : Foo) → Bar2 (foo x (bar x) (bar2 x))<br><br>bar2-temp = bar2<br></blockquote><div><br></div><div>It seems a little silly that constructors cannot be references before they are defined, even when inside a mutual block. There also seems to be a difference between the old- and new-style mutual blocks when referencing datatypes. Maybe we could improve Agda to handle situations like this more uniformly?<br><br></div><div>cheers,<br></div><div>Jesper <br></div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Mar 15, 2016 at 4:03 PM, Simon Boulier <span dir="ltr"><<a href="mailto:simon.boulier@ens-rennes.fr" target="_blank">simon.boulier@ens-rennes.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<br>
This way?<br>
<blockquote><small><tt>mutual</tt><tt><br>
</tt><tt> data Foo : Set where</tt><span class=""><tt><br>
</tt><tt> foo : (x : Foo) → Bar x → Bar2 x → Foo</tt><tt><br>
</tt><tt><br>
</tt></span><tt> data Bar : Foo → Set where</tt><span class=""><tt><br>
</tt><tt> bar : (x : Foo) → Bar x</tt><tt><br>
</tt><tt> bar' : (x : Foo) → Bar (foo x (bar x) (bar2 x))</tt><tt><br>
</tt><tt><br>
</tt></span><tt> data Bar2 : Foo → Set where</tt><span class=""><tt><br>
</tt><tt> bar2 : (x : Foo) → Bar2 x</tt><tt><br>
</tt><tt> bar2' : (x : Foo) → Bar2 (foo x (bar x) (bar2 x))</tt></span></small><br>
</blockquote>
I doesn't seem to change anything for me...<br>
Agda still complains that bar2 is not in scope when type checking
bar'.<div><div class="h5"><br>
<br>
<br>
<br>
<div>Le 15/03/2016 15:50, Dr. ERDI Gergo a
écrit :<br>
</div>
<blockquote type="cite">On Tue, 15 Mar 2016, Simon Boulier wrote:
<br>
<br>
<blockquote type="cite">Is it a way to type check the following:
<br>
data Foo : Set
<br>
data Bar : Foo → Set
<br>
data Bar2 : Foo → Set
<br>
<br>
data Foo where
<br>
foo : (x : Foo) → Bar x → Bar2 x → Foo
<br>
</blockquote>
...
<br>
<br>
If you put them in a 'mutual' block, that should be OK (as long as
positivity blah blah blah).<br>
</blockquote>
<br>
</div></div></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>