<div dir="ltr"><div>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.<br><br></div>-- Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Nov 25, 2017 at 11:53 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">> Are non-linear patterns a new feature? Or a bug. If they are a feature,<br>
> what is their specified behaviour?<br>
<br></span>
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.<br>
<br>
--Andreas<div class="HOEnZb"><div class="h5"><br>
<br>
On 24.11.2017 22:48, Martín Hötzel Escardó wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I was working at the University and had this to compile in my computer there, with 2.6.0:<br>
<br>
```<br>
yoneda-lemma : {X : U} {x : X} {A : PrShf X} (η : Nat (Hom x) A)<br>
              → yoneda-nat A (yoneda-elem A η) ≈ η<br>
yoneda-lemma {X} {x} {A} η x (idp x) = idp (yoneda-elem A η)<br>
```<br>
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.<br>
<br>
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.<br>
<br>
Are non-linear patterns a new feature? Or a bug. If they are a feature, what is their specified behaviour?<br>
<br>
Martin<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote>
<br>
<br></div></div><span class="HOEnZb"><font color="#888888">
-- <br>
Andreas Abel  <><      Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~ab<wbr>ela/</a></font></span><div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>