[Agda] Coinductive records and separate files in Agda

[Jesper Cockx]

Hi Bill,

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.

-- Jesper

On Thu, Jan 16, 2020 at 3:53 PM William Harrison <
william.lawrence.harrison at gmail.com> wrote:

> Hi-
>
>     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.
>
> 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):
>
> record Stream {ℓ} (A : Set ℓ) : Set ℓ where
>   coinductive
>   field headStr : A
>         tailStr : Stream A
> open Stream; S = Stream
>
> zeros : Stream ℕ
> headStr zeros = 0
> tailStr zeros = zeros
>
> record Derp (A B : Set) : Set where
>   field
>     fld1 : A
>     fld2 : B
>
> In the second file (Records2.agda), I load Records1 (hiding zeros):
>
> open import Records1 hiding (zeros)
>
> -- Use of non-coinductive record in this file works fine:
> foo : Derp ℕ ℕ
> foo = record { fld1 = 0 ; fld2 = 1 }
>
> -- The identical zeros definition generates an odd error:
> zeros : Stream ℕ
> headStr zeros = 0
> tailStr zeros = zeros
>
> That error is:
>
> <local-file-path>/Records2.agda:12,1-14
> Could not parse the left-hand side headStr zeros
> Operators used in the grammar:
>   None
> when scope checking the left-hand side headStr zeros in the
> definition of zeros
>
> 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.
>
> Thanks,
> Bill
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200116/6e242d10/attachment.html>