As-pattern for and within implicit arguments

[jonaprieto]

The formatter (v0.5.1-dev) changes as-patterns as in the following example.

a : {A : Type} → A × Nat → Nat
-  | {A'@_} p@(x, s@zero) := snd p + 1
+  | A'@{_} p@(x, s@zero) := snd p + 1
  | p@(x, s@_) := snd p + 1;

While the change breaks the code atm, I think this is fine, i.e.,
an implicit pattern expression can be named in the following way.

f : {x : _} -> ...:=
  | y@{_} := ...;

One may need to name inner patterns as well, so the following should be also
permitted.

f : {x : Ind} -> ...:=
  | ...
  | y@{cons1 x1 z@(cons x2 xs)} := ...;

[jonaprieto]

The change done by the formatter in v0.5.1 was a bug, recently fixed by #2486. We are not interested in changing its syntax in the short term.