<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 15 November 2014 12:19, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div id=":vr" class="" style="overflow:hidden">This is on the language change.<br>
For example, I have<br>
<br>
-------------------------------------------------------------------------<br>
module Membership2 {α α= : Level} (A : Setoid α α=)<br>
  where<br>
  ...<br>
<br>
  x∈del-x→anyRepeats : (_≟_ : Decidable₂ _≈_) → ∀ {x xs} →<br>
                                        x ∈ del _≟_ x xs → AnyRepeats xs<br>
<br>
  x∈del-x→anyRepeats _   {_} {[]}     ()<br>
  x∈del-x→anyRepeats _≟_ {x} {y ∷ xs} x∈del-x-y:xs  with x ≟ y<br>
  ...<br>
      | yes x=y =  hereRep y∈xs   where  x∈xs : x ∈ xs<br>
                                         x∈xs = x∈del-x-y:xs<br>
<br>
                                         y∈xs = cong₁∈ x=y x∈xs<br>
  ... | no x≉y =  thereRep anyRep-xs<br>
                  where<br>
                  x∈y:del-xs :  x ∈ y ∷ (del _≟_ x xs)<br>
                  x∈y:del-xs =  x∈del-x-y:xs<br>
<br>
                  x∈del-xs : x ∈ del _≟_ x xs<br>
                  x∈del-xs with  x∈y:del-xs<br>
                  ...           | here x=y       = ⊥-elim $ x≉y x=y<br>
                  ...           | there x∈del-xs = x∈del-xs<br>
<br>
                  anyRep-xs : AnyRepeats xs<br>
                  anyRep-xs = x∈del-x→anyRepeats _≟_ x∈del-xs<br>
--------------------------------------------------------------------------<br>
<br>
This means a lemma:<br>
     &quot;if  x  is in  (delete x xs),  then  xs  has a repetition in it&quot;.<br>
<br>
It is accepted in  Agda 2.4.2  and is forbidden in  Agda 2.4.2.1 :<br>
<br>
&quot;Cannot `with` on variable x∈del-x-y:xs bound in a module telescope<br>
(or patterns of a parent clause)<br>
when inferring the type of x∈del-x-y:xs<br>
&quot;.<br>
<br>
I wonder: how to fix the code?</div></blockquote></div><br><span id="result_box" class="" lang="en"><span class="">I didn&#39;t look</span> <span class="">in detail</span> your <span class="">example but</span></span> in <a href="https://code.google.com/p/agda/issues/detail?id=1355">https://code.google.com/p/agda/issues/detail?id=1355</a> (comment #2) there is an example of solution for this kind of error (you need the development version of Agda for type-checking the modules used in this issue).<br><br></div><div class="gmail_extra">-- <br><div class="gmail_signature"><div dir="ltr">Andrés<br></div></div>
</div></div>