<div dir="ltr"><div>Hi Bill,</div><br><div>I think you need to write "open Stream public" instead of "open Stream" if you want the fields to be in scope in other modules (or you can re-open the record in the other module). Maybe the error message could be improved to indicate that there is a projection with name headStr but it is only in scope under its qualified name.<br></div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 16, 2020 at 3:53 PM William Harrison <<a href="mailto:william.lawrence.harrison@gmail.com">william.lawrence.harrison@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><span style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">Hi-</span><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">    I’m not able to separate the definition of a coinductive record type from definitions using that type. I’ve attached two files giving a minimal example of the issue. I’m trying to determine if I’m doing something wrong or if I’ve discovered a bug/feature.</div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">The first file (Records1.agda) gives the usual definition of a stream using coinductive record syntax and a non-coinductive record; respectively, these are Stream and Derp. I can define within Record1 particular Streams (e.g., zeros below):</div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><div><font face="Courier New">record Stream {ℓ} (A : Set ℓ) : Set ℓ where</font></div><div><font face="Courier New">  coinductive</font></div><div><font face="Courier New">  field headStr : A</font></div><div><font face="Courier New">        tailStr : Stream A</font></div><div><font face="Courier New">open Stream; S = Stream</font></div><div><font face="Courier New"><br></font></div><div><font face="Courier New">zeros : Stream ℕ</font></div><div><font face="Courier New">headStr zeros = 0</font></div><div><font face="Courier New">tailStr zeros = zeros</font></div><div><font face="Courier New"><br></font></div><div><font face="Courier New">record Derp (A B : Set) : Set where</font></div><div><font face="Courier New">  field</font></div><div><font face="Courier New">    fld1 : A</font></div><div><font face="Courier New">    fld2 : B</font></div></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">In the second file (Records2.agda), I load Records1 (hiding zeros):</div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><div><font face="Courier New">open import Records1 hiding (zeros)</font></div><div><font face="Courier New"><br></font></div><div><font face="Courier New">-- Use of non-coinductive record in this file works fine:</font></div><div><font face="Courier New">foo : Derp ℕ ℕ</font></div><div><font face="Courier New">foo = record { fld1 = 0 ; fld2 = 1 }</font></div><div><font face="Courier New"><br></font></div><div><font face="Courier New">-- The identical zeros definition generates an odd error:</font></div><div><font face="Courier New">zeros : Stream ℕ</font></div><div><font face="Courier New">headStr zeros = 0</font></div><div><font face="Courier New">tailStr zeros = zeros</font></div></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">That error is:</div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><div><font face="Courier New"><local-file-path>/Records2.agda:12,1-14</font></div><div><font face="Courier New">Could not parse the left-hand side headStr zeros</font></div><div><font face="Courier New">Operators used in the grammar:</font></div><div><font face="Courier New">  None</font></div><div><font face="Courier New">when scope checking the left-hand side headStr zeros in the</font></div><div><font face="Courier New">definition of zeros</font></div></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">Am I doing something wrong here? Is there some way to separate coinductive record type declarations and particular values of those types in distinct files? If it matters, I’m using Agda 2.6.0.1, although I’ve seen this same behavior in earlier versions of Agda.</div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br></div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">Thanks,</div><div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">Bill</div><br style="color:rgb(0,0,0);font-family:-webkit-standard"></div></div>
_______________________________________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>