[Agda] rewriting and parameterized modules

[Jesper Cockx]

This is a bug in Agda, I've added it to the issue tracker:
https://github.com/agda/agda/issues/2606

Working on a fix...

-- Jesper

On Fri, Jun 16, 2017 at 5:19 PM, Ambrus Kaposi <kaposi.ambrus at gmail.com>
wrote:

> Hi Agda Developers,
>
> I don't understand why the following module doesn't typecheck. The error is
>
> β  is not a legal rewrite rule, since the left-hand side  f a  reduces
> to  f a  when checking the pragma REWRITE β
>
> If I remove the X parameters from the m1 and m2 modules, it works. It
> also works when m1 and m2 are merged. But I'd like to use separate
> parameterised modules.
>
> What is the explanation for this behaviour?
>
> Many thanks,
> Ambrus
>
>
>
>
> {-# OPTIONS --rewriting #-}
>
> module a where
>
> postulate
>   _~_ : {A : Set} → A → A → Set
>
> {-# BUILTIN REWRITE _~_ #-}
>
> module m1 (X : Set) where
>
>   postulate
>     A B : Set
>     a : A
>     b : B
>     f : A → B
>
> module m2 (X : Set) where
>
>   open m1 X
>
>   postulate
>     β : f a ~ b
>
>   {-# REWRITE β #-}
> _______________________________________________
> 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/20170616/e6ce6394/attachment.html>