<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">On Tue, Sep 13, 2016 at 8:40 PM, Simon Boulier <span dir="ltr">&lt;<a href="mailto:simon.boulier@ens-rennes.fr" target="_blank">simon.boulier@ens-rennes.fr</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  

    
  
  <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>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>