[Agda] dotted pattern for pair

[Ulf Norell]

I filed https://github.com/agda/agda/issues/2196 where we can continue the
discussion.

/ Ulf

On Mon, Sep 19, 2016 at 8:03 PM, Andreas Abel <abela at chalmers.se> wrote:

> Hi Sergei,
>
> thanks for alerting us?  Could you please provide a self-contained example?
>
> Thanks,
> Andreas
>
>
> On 19.09.2016 14:03, Sergei Meshveliani wrote:
>
>> Hi,
>>
>> For _=p_ being a coordinatewise equality on  ℕ × ℕ,  the function
>>
>>   pr :  pairToNZ Preserves _=p_ ⟶ _='p_
>>   pr {(n , e)} {.(n , e)} (PE.refl , PE.refl) =  ...
>>
>> is type-checked in Agda-2.5.1.1 and is not type-checked in Development
>> Agda of September 16, 2016.
>> The latter version does not accept this dotted pattern and insists on
>> the pattern  {(.n , e.)}  instead.
>>
>> I point out the difference, for any occasion.
>>
>> Regards,
>>
>> ------
>> 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/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160919/888e06de/attachment.html