[Agda] dotted pattern for pair

[Andreas Abel]

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/