[Agda] dotted patterns

[Jesper Cockx]

To expand a little on that: the intended semantics is that in the new
version of Agda you will be allowed to write `x` exactly where you would
previously be allowed to write `.x`. In the current development version the
implementation is still a bit too liberal and allows you to write `x` in
place of any dot pattern `.t`, but this will be fixed before the next
release.

-- Jesper

On Sat, Nov 25, 2017 at 11:53 AM, Andreas Abel <abela at chalmers.se> wrote:

> > Are non-linear patterns a new feature? Or a bug. If they are a feature,
> > what is their specified behaviour?
>
> Short answer:  The plan is that in future versions of Agda (like the
> current development versions) you can drop the dots in front of variables.
> Agda will internally place the dots to preserve the linearity of the
> matching.  You can still manually place the dots.
>
> --Andreas
>
>
> On 24.11.2017 22:48, Martín Hötzel Escardó wrote:
>
>> I was working at the University and had this to compile in my computer
>> there, with 2.6.0:
>>
>> ```
>> yoneda-lemma : {X : U} {x : X} {A : PrShf X} (η : Nat (Hom x) A)
>>               → yoneda-nat A (yoneda-elem A η) ≈ η
>> yoneda-lemma {X} {x} {A} η x (idp x) = idp (yoneda-elem A η)
>> ```
>> But this was an accident with very old code, in which I decided to make
>> some implicit argument explicit, and I forgot add the required dots.
>>
>> At home, now, in another machine with Agda 2.6.0, it didn't compile. But
>> I pulled the last version of Agda (2.6.0-3b39f0f) and it does compile with
>> that.
>>
>> Are non-linear patterns a new feature? Or a bug. If they are a feature,
>> what is their specified behaviour?
>>
>> Martin
>>
>> _______________________________________________
>> 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://www.cse.chalmers.se/~abela/
>
> _______________________________________________
> 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/20171125/1b671957/attachment.html>