Analogue to Agda's `{!...!}`

Stream: new members

[Andreas Nuyts]

Hi!
In Agda, you can have a goal with contents (some code that was there before you decided to put a goal instead, or some comments in words explaining why the goal is (in)feasable; basically anything and it will be ignored).
The syntax is {!random goal contents!}.
I understand that the Lean way of having goals is either _ or sorry. Is there an equivalent of Agda's {!...!}?

[Aaron Liu]

I guess you can put a regular comment?

[Eric Wieser]

_ /- comment -/?