Syntax for naming subpatterns

[lukaszcz]

Do we have a syntax for naming subpatterns? I don't think so. It's an extremely useful feature and I would advocate including it.

Then we need a syntax for it, possibly a reserved symbol to indicate the name.

Some options:

f : {A : Type} -> List (List A) -> List A;
f (cons x@(cons _ _) nil) := x;
f (cons x#(cons _ _) nil) := x;

We don't want to enforce spaces around the "naming" symbol (related to issues #1528, #1495).

[lukaszcz]

Even Agda has those without forcing the user to write the damn spaces: https://agda.readthedocs.io/en/v2.6.0.1/language/function-definitions.html#as-patterns

[janmasrovira]

@lukaszcz We discussed this issue before you joined. We want to have as-patterns using the Haskell syntax that you already displayed above: x@(cons _ _). It's not in the language yet because we didn't see it as a priority so we never implemented it

[lukaszcz]

I opened the issue because it came up while designing the complex "Match" in the core. It's not a big deal to have as-patterns in the core, so I think it's better to add them now than later change the data structure.

Is it fine if I just add "@" to reservedSymbols? You don't use it anywhere, you plan to use it for as-patterns (which probably requires making it reserved anyway), and then I could use it in JVC files for as-patterns without the spaces around.

[janmasrovira]

Is it fine if I just add "@" to reservedSymbols? You don't use it anywhere, you plan to use it for as-patterns (which probably requires making it reserved anyway), and then I could use it in JVC files for as-patterns without the spaces around.

please go ahead.