Public open between two fields

[UlfNorell]

From vitus...@gmail.com on November 07, 2013 22:42:35

Relevant code:

data ≡ {A : Set} (x : A) : A → Set where refl : x ≡ x

module Foo {A : Set} (f : A → A) where foo : A → A foo x = f (f x)

record R (A : Set) : Set where field f : A → A

open Foo f public

field proof : ∀ x → foo x ≡ f x

This code produces (seemingly) puzzling error message:

Not a valid let-declaration when scope checking ...

This issue is sort of both a feature request and a bug report. Ideally, you could publicly open a module between two fields; as far as I know, the only workaround is to either use Foo.foo f x and open the module once at the end or to open the module twice:

record R (A : Set) : Set where field f : A → A

open Foo f

field proof : ∀ x → foo x ≡ f x

open Foo f public

If this is not possible, the error message should be made clearer.

Original issue: http://code.google.com/p/agda/issues/detail?id=946

[UlfNorell]

From ulf.nor...@gmail.com on November 07, 2013 23:49:59

Status: Duplicate
Mergedinto: 434

[UlfNorell]

From ulf.nor...@gmail.com on November 07, 2013 23:51:09

Gah, why isn't the MergedInto field a link? Link: Issue 434 .

[UlfNorell]

From guillaum...@gmail.com on November 08, 2013 09:52:42

There is a link at the top left of the page (in the "position:fixed" div).

[UlfNorell]

From vitus...@gmail.com on November 08, 2013 10:11:19

This concrete example (open public between two and more fields) has been fixed by the fix to Issue 532 (I must have missed that one, sorry).