@(λ {x}, ...) not supported

[digama0]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

It is possible to produce terms that have @ annotations on lambdas, but the parser doesn't recognize them, leading to a situation where pp.all produces printouts that are not syntactically correct.

def T : Type := by have := (λ {x : unit}, unit); exact @this ()
set_option pp.all true
#print T -- def T : Type := @(λ {x : unit}, unit) unit.star

def T' : Type := @(λ {x : unit}, unit) unit.star -- error