[Agda] variables not bound with REWRITE pragma

[Jesper Cockx]

I think it's the following commit that fixed this problem:
https://github.com/agda/agda/commit/167438712b3ea5e363078738fe856860574799a7
It's from 22 April, *just* after the release of 2.5.1, so you need to
install Agda from source if you want to use it now (or otherwise wait until
the next release).

Jesper

On Tue, Sep 13, 2016 at 8:49 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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/943a03c7/attachment.html