<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 15 November 2014 12:19, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>
"if x is in (delete x xs), then xs has a repetition in it".<br>
<br>
It is accepted in Agda 2.4.2 and is forbidden in Agda 2.4.2.1 :<br>
<br>
"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>
".<br>
<br>
I wonder: how to fix the code?</div></blockquote></div><br><span id="result_box" class="" lang="en"><span class="">I didn'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>