[Agda] ANNOUNCE: Agda 2.4.2.1

[Andrés Sicard-Ramírez]

On 15 November 2014 12:19, Sergei Meshveliani <mechvel at botik.ru> wrote:

> This is on the language change.
> For example, I have
>
> -------------------------------------------------------------------------
> module Membership2 {α α= : Level} (A : Setoid α α=)
>   where
>   ...
>
>   x∈del-x→anyRepeats : (_≟_ : Decidable₂ _≈_) → ∀ {x xs} →
>                                         x ∈ del _≟_ x xs → AnyRepeats xs
>
>   x∈del-x→anyRepeats _   {_} {[]}     ()
>   x∈del-x→anyRepeats _≟_ {x} {y ∷ xs} x∈del-x-y:xs  with x ≟ y
>   ...
>       | yes x=y =  hereRep y∈xs   where  x∈xs : x ∈ xs
>                                          x∈xs = x∈del-x-y:xs
>
>                                          y∈xs = cong₁∈ x=y x∈xs
>   ... | no x≉y =  thereRep anyRep-xs
>                   where
>                   x∈y:del-xs :  x ∈ y ∷ (del _≟_ x xs)
>                   x∈y:del-xs =  x∈del-x-y:xs
>
>                   x∈del-xs : x ∈ del _≟_ x xs
>                   x∈del-xs with  x∈y:del-xs
>                   ...           | here x=y       = ⊥-elim $ x≉y x=y
>                   ...           | there x∈del-xs = x∈del-xs
>
>                   anyRep-xs : AnyRepeats xs
>                   anyRep-xs = x∈del-x→anyRepeats _≟_ x∈del-xs
> --------------------------------------------------------------------------
>
> This means a lemma:
>      "if  x  is in  (delete x xs),  then  xs  has a repetition in it".
>
> It is accepted in  Agda 2.4.2  and is forbidden in  Agda 2.4.2.1 :
>
> "Cannot `with` on variable x∈del-x-y:xs bound in a module telescope
> (or patterns of a parent clause)
> when inferring the type of x∈del-x-y:xs
> ".
>
> I wonder: how to fix the code?
>

I didn't look in detail your example but in
https://code.google.com/p/agda/issues/detail?id=1355 (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).

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141115/2294eab8/attachment.html