[Agda] variables not bound with REWRITE pragma

[Jesper Cockx]

Hi Simon,

Which version of Agda are you using? Your example is accepted by my
currently installed development version of Agda, so I guess that this has
already been fixed. Rewriting is still an experimental feature so you
should expect sometimes frequent changes.

cheers,
Jesper

On Tue, Sep 13, 2016 at 8:40 PM, Simon Boulier <simon.boulier at ens-rennes.fr>
wrote:

> Hi,
>
> I am trying to play with with the REWRITE pragma.
>
> In the following example:
>
> {-# OPTIONS --rewriting #-}
>
> postulate
>   Z : Set
>   z : Set → Z
>   z∀ : (A : Set)(B : A → Set) → Z
>
> postulate _↦_ : Z → Z → Set
> {-# BUILTIN REWRITE _↦_ #-}
>
> postulate z∀_z∀ : (A : Set)(B : A → Set) →   z (∀ (x : A) → B x) ↦ z∀ A (λ
> (x : A) → B x)
> {-# REWRITE z∀_z∀ #-}
>
> Agda complains:
>
> z∀_z∀  is not a legal rewrite rule, since the following variables are not
> bound by the left hand side:  B
> when checking the pragma REWRITE z∀_z∀
>
> whereas it works if I make B not depending on A in z∀_z∀.
>
> Is it a bug, or did I miss something? Is their a workaround?
>
> Cheers,
>
> Simon
>
> _______________________________________________
> 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/20160913/37773e03/attachment.html