<div dir="ltr"><div dir="ltr"><span style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">Hi-</span><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" 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 class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" 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 class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><div class="gmail-"><font face="Courier New" class="gmail-">record Stream {ℓ} (A : Set ℓ) : Set ℓ where</font></div><div class="gmail-"><font face="Courier New" class="gmail-">  coinductive</font></div><div class="gmail-"><font face="Courier New" class="gmail-">  field headStr : A</font></div><div class="gmail-"><font face="Courier New" class="gmail-">        tailStr : Stream A</font></div><div class="gmail-"><font face="Courier New" class="gmail-">open Stream; S = Stream</font></div><div class="gmail-"><font face="Courier New" class="gmail-"><br class="gmail-"></font></div><div class="gmail-"><font face="Courier New" class="gmail-">zeros : Stream ℕ</font></div><div class="gmail-"><font face="Courier New" class="gmail-">headStr zeros = 0</font></div><div class="gmail-"><font face="Courier New" class="gmail-">tailStr zeros = zeros</font></div><div class="gmail-"><font face="Courier New" class="gmail-"><br class="gmail-"></font></div><div class="gmail-"><font face="Courier New" class="gmail-">record Derp (A B : Set) : Set where</font></div><div class="gmail-"><font face="Courier New" class="gmail-">  field</font></div><div class="gmail-"><font face="Courier New" class="gmail-">    fld1 : A</font></div><div class="gmail-"><font face="Courier New" class="gmail-">    fld2 : B</font></div></div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" 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 class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><div class="gmail-"><font face="Courier New" class="gmail-">open import Records1 hiding (zeros)</font></div><div class="gmail-"><font face="Courier New" class="gmail-"><br class="gmail-"></font></div><div class="gmail-"><font face="Courier New" class="gmail-">-- Use of non-coinductive record in this file works fine:</font></div><div class="gmail-"><font face="Courier New" class="gmail-">foo : Derp ℕ ℕ</font></div><div class="gmail-"><font face="Courier New" class="gmail-">foo = record { fld1 = 0 ; fld2 = 1 }</font></div><div class="gmail-"><font face="Courier New" class="gmail-"><br class="gmail-"></font></div><div class="gmail-"><font face="Courier New" class="gmail-">-- The identical zeros definition generates an odd error:</font></div><div class="gmail-"><font face="Courier New" class="gmail-">zeros : Stream ℕ</font></div><div class="gmail-"><font face="Courier New" class="gmail-">headStr zeros = 0</font></div><div class="gmail-"><font face="Courier New" class="gmail-">tailStr zeros = zeros</font></div></div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">That error is:</div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><div class="gmail-"><font face="Courier New" class="gmail-"><local-file-path>/Records2.agda:12,1-14</font></div><div class="gmail-"><font face="Courier New" class="gmail-">Could not parse the left-hand side headStr zeros</font></div><div class="gmail-"><font face="Courier New" class="gmail-">Operators used in the grammar:</font></div><div class="gmail-"><font face="Courier New" class="gmail-">  None</font></div><div class="gmail-"><font face="Courier New" class="gmail-">when scope checking the left-hand side headStr zeros in the</font></div><div class="gmail-"><font face="Courier New" class="gmail-">definition of zeros</font></div></div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" 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 class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px"><br class="gmail-"></div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">Thanks,</div><div class="gmail-" style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px">Bill</div><br class="gmail-Apple-interchange-newline" style="color:rgb(0,0,0);font-family:-webkit-standard"></div></div>