[Agda] dotted patterns

[Andreas Abel]

 > 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/