[Agda] "not in scope" without "does not export"
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Jun 23 16:41:46 CEST 2020
Thanks, this is a regression, see: https://github.com/agda/agda/issues/4773
Should be fixed in Agda 2.6.2.
On 2020-06-20 11:57, mechvel at scico.botik.ru wrote:
> Dear Agda developers,
>
> For the below program
> (not self-contained, non-standard records for algebra)
>
> Agda 2.6.1 reports
> "Not in scope:
> Foo
> ".
>
> May be, it rather needs to report
> "The module OfCommutativeMonoid does not export commutativeSemigroup"
> ?
> (the word `public' is missed in the code).
>
>
> module OfCommutativeMonoid (CM : CommutativeMonoid) where
> open CommutativeMonoid CM using (commutativeSemigroup)
>
> module OfSemiring (R : Semiring) where
> open Semiring R using (+-commutativeMonoid)
>
> module OfCommutativeSemiring (R : CommutativeSemiring)
> where
> open CommutativeSemiring R using (*-commutativeMonoid)
> open OfCommutativeMonoid *-commutativeMonoid using ()
> renaming (commutativeSemigroup to Foo)
>
> debug : CommutativeSemigroup
> debug = Foo
>
>
> Regards,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list