[Agda] dotted patterns

[Martín Hötzel Escardó]

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

[Andreas Abel]

Post by Martín Hötzel Escardó
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

Post by Martín Hötzel Escardó
I was working at the University and had this to compile in my computer
```
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by Andreas Abel

Post by Martín Hötzel Escardó
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

Post by Martín Hötzel Escardó
I was working at the University and had this to compile in my computer
```
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
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
http://www.cse.chalmers.se/~abela/
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda