[Agda] ANNOUNCE: Agda 2.4.2.1

[Andreas Abel]

Well, you can patttern-match on  x∈del-x-y:xs  directly after the `with` 
on  x ≟ y (in this case, do not use the notation ... for ellipsis), no 
need to `with` on it.

On 16.11.14 1:19 AM, Sergei Meshveliani wrote:
> On Fri, 2014-11-14 at 19:21 -0500, Andrés Sicard-Ramírez wrote:
>> Hi,
>>
>> Agda 2.4.2.1 has been released.
>>
>> [..]
>
>
> 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?
> Does not this above code look natural?
>
> (I fear, that there are many similar places in my application).
>
> Thanks,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/