<div dir="ltr"><div>I think it's the following commit that fixed this problem: <a href="https://github.com/agda/agda/commit/167438712b3ea5e363078738fe856860574799a7">https://github.com/agda/agda/commit/167438712b3ea5e363078738fe856860574799a7</a> 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).<br><br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Sep 13, 2016 at 8:49 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Hi Simon,<br><br></div>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.<br><br></div>cheers,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Tue, Sep 13, 2016 at 8:40 PM, Simon Boulier <span dir="ltr"><<a href="mailto:simon.boulier@ens-rennes.fr" target="_blank">simon.boulier@ens-rennes.fr</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
<div text="#000000" bgcolor="#FFFFFF">
<p>Hi,</p>
<p>I am trying to play with with the REWRITE pragma.</p>
<p>In the following example:</p>
<blockquote>
<p><font size="-1"><tt>{-# OPTIONS --rewriting #-}</tt><tt><br>
</tt><tt><br>
</tt><tt>postulate</tt><tt><br>
</tt><tt> Z : Set</tt><tt><br>
</tt><tt> z : Set → Z</tt><tt><br>
</tt><tt> z∀ : (A : Set)(B : A → Set) → Z</tt><tt><br>
</tt><tt><br>
</tt><tt>postulate _↦_ : Z → Z → Set</tt><tt><br>
</tt><tt>{-# BUILTIN REWRITE _↦_ #-}</tt><tt><br>
</tt><tt><br>
</tt><tt>postulate z∀_z∀ : (A : Set)(B : A → Set) → z (∀ (x
: A) → B x) ↦ z∀ A (λ (x : A) → B x)</tt><tt><br>
</tt><tt>{-# REWRITE z∀_z∀ #-}</tt></font><br>
</p>
</blockquote>
<p>Agda complains:</p>
<blockquote>
<p><font size="-1"><tt>z∀_z∀ is not a legal rewrite rule, since
the following variables are not bound by the left hand
side: B</tt><br>
</font>
<font size="-1"><tt>when checking the pragma REWRITE z∀_z∀</tt></font></p>
</blockquote>
<p>whereas it works if I make B not depending on A in <font size="-1">z∀_z∀.</font></p>
<p>Is it a bug, or did I miss something? Is their a workaround?<br>
</p>
<p>Cheers,</p>
<p>Simon<font size="-1"><tt><br>
</tt></font></p>
</div>
<br></div></div>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>